From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 28 Aug 2012 08:55:32 +0000 (+0000)
Subject: pattern arguments where printed in reverse order
X-Git-Tag: make_still_working~1534
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=99bd9f6d6f65a844149236933524ffdf95627a4c

pattern arguments where printed in reverse order
---

diff --git a/matita/components/ng_kernel/nCicExtraction.ml b/matita/components/ng_kernel/nCicExtraction.ml
index fb98942b6..a091f0c8a 100644
--- a/matita/components/ng_kernel/nCicExtraction.ml
+++ b/matita/components/ng_kernel/nCicExtraction.ml
@@ -801,18 +801,18 @@ let rec pretty_print_type status ctxt =
    | TAppl tl -> String.concat " " (List.map (pretty_print_type status ctxt) tl)
 
 let pretty_print_term_context status ctx1 ctx2 =
- let name_context, res =
+ let name_context, rev_res =
   List.fold_right
-    (fun el (ctx1,res) ->
+    (fun el (ctx1,rev_res) ->
       match el with
-         None -> ""@::ctx1,res
-       | Some (name,`OfKind _) -> name@::ctx1,res
+         None -> ""@::ctx1,rev_res
+       | Some (name,`OfKind _) -> name@::ctx1,rev_res
        | Some (name,`OfType typ) ->
           let name,ctx1 = name@:::ctx1 in
            name::ctx1,
-            ("(" ^ name ^ " :: " ^ pretty_print_type status ctx1 typ ^ ")")::res
+            ("(" ^ name ^ " :: " ^ pretty_print_type status ctx1 typ ^ ")")::rev_res
     ) ctx2 (ctx1,[]) in
-  name_context, String.concat " " res
+  name_context, String.concat " " (List.rev rev_res)
 
 let rec pretty_print_term status ctxt =
   function