From c742f5b1450507df01cb0379d85b4170ddf6cad5 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 2 Aug 2012 20:05:10 +0000 Subject: [PATCH] Bug fixed: the context generated by l.h.s. binders was appended in wrong order. --- matita/components/ng_kernel/nCicExtraction.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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) -- 2.39.2