From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 2 Aug 2012 20:05:10 +0000 (+0000)
Subject: Bug fixed: the context generated by l.h.s. binders was appended in wrong order.
X-Git-Tag: make_still_working~1569
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c742f5b1450507df01cb0379d85b4170ddf6cad5;p=helm.git

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 4280f7388..76b53f363 100644
--- 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)