From 99bd9f6d6f65a844149236933524ffdf95627a4c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 28 Aug 2012 08:55:32 +0000 Subject: [PATCH] pattern arguments where printed in reverse order --- matita/components/ng_kernel/nCicExtraction.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/matita/components/ng_kernel/nCicExtraction.ml b/matita/components/ng_kernel/nCicExtraction.ml index fb98942b6..a091f0c8a 100644 --- a/matita/components/ng_kernel/nCicExtraction.ml +++ b/matita/components/ng_kernel/nCicExtraction.ml @@ -801,18 +801,18 @@ let rec pretty_print_type status ctxt = | TAppl tl -> String.concat " " (List.map (pretty_print_type status ctxt) tl) let pretty_print_term_context status ctx1 ctx2 = - let name_context, res = + let name_context, rev_res = List.fold_right - (fun el (ctx1,res) -> + (fun el (ctx1,rev_res) -> match el with - None -> ""@::ctx1,res - | Some (name,`OfKind _) -> name@::ctx1,res + None -> ""@::ctx1,rev_res + | Some (name,`OfKind _) -> name@::ctx1,rev_res | Some (name,`OfType typ) -> let name,ctx1 = name@:::ctx1 in name::ctx1, - ("(" ^ name ^ " :: " ^ pretty_print_type status ctx1 typ ^ ")")::res + ("(" ^ name ^ " :: " ^ pretty_print_type status ctx1 typ ^ ")")::rev_res ) ctx2 (ctx1,[]) in - name_context, String.concat " " res + name_context, String.concat " " (List.rev rev_res) let rec pretty_print_term status ctxt = function -- 2.39.2