Bug fixed: the context generated by l.h.s. binders was appended in wrong order.

diff --git a/matita/components/ng_kernel/nCicExtraction.ml b/matita/components/ng_kernel/nCicExtraction.ml
index 4280f7388205ceb6f9e49f02e45f9f574e3c10dd..76b53f363658f46a42e70898ead686a989001787 100644 (file)
--- a/matita/components/ng_kernel/nCicExtraction.ml
+++ b/matita/components/ng_kernel/nCicExtraction.ml
@@ -624,7 +624,7 @@ let rec pp_term status ctx =
         let pattern,body =
          (*CSC: BUG avoid name clashes *)
          String.concat " " (String.capitalize name::bound_names),
-         pp_term status (bound_names@ctx) rhs
+         pp_term status ((List.rev bound_names)@ctx) rhs
         in
          "  " ^ pattern ^ " -> " ^ body
      ) patterns)