From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 28 Aug 2012 08:46:19 +0000 (+0000)
Subject: Bug fixed: rhs in match were printed in wrong context.
X-Git-Tag: make_still_working~1535
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=97f8b4052e981701727dcc8c8b625fe66e9d4f60;p=helm.git

Bug fixed: rhs in match were printed in wrong context.
---

diff --git a/matita/components/ng_kernel/nCicExtraction.ml b/matita/components/ng_kernel/nCicExtraction.ml
index afe79e7af..fb98942b6 100644
--- a/matita/components/ng_kernel/nCicExtraction.ml
+++ b/matita/components/ng_kernel/nCicExtraction.ml
@@ -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)