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 afe79e7af62c3966ccd1282b8de0b0ef889ffc91..fb98942b6d4a6241c9ffd9732cedf9fb08a1e843 100644 (file)
--- 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)