From 97f8b4052e981701727dcc8c8b625fe66e9d4f60 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 28 Aug 2012 08:46:19 +0000 Subject: [PATCH] Bug fixed: rhs in match were printed in wrong context. --- matita/components/ng_kernel/nCicExtraction.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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) -- 2.39.2