pattern arguments where printed in reverse order

[helm.git] / matita / components / ng_kernel / nCicExtraction.ml

diff --git a/matita/components/ng_kernel/nCicExtraction.ml b/matita/components/ng_kernel/nCicExtraction.ml
index afe79e7af62c3966ccd1282b8de0b0ef889ffc91..a091f0c8a7fb824cef029b11602bbc63a31756d4 100644 (file)
--- 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
@@ -843,10 +843,10 @@ let rec pretty_print_term status ctxt =
              (fun (bound_names,rhs) i ->
                let ref = NReference.mk_constructor (i+1) r in
                let name = pp_ref status ref in
-               let names,bound_names =
+               let ctxt,bound_names =
                 pretty_print_term_context status ctxt bound_names in
                let body =
-                pretty_print_term status ((List.rev names)@ctxt) rhs
+                pretty_print_term status ctxt rhs
                in
                  "  " ^ name ^ " " ^ bound_names ^ " -> " ^ body
              ) pl)