From 82ef03cc4bc4752284348127ed0303008b95ee79 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 15 Nov 2002 18:42:13 +0000 Subject: [PATCH] Order of the generated metavariables for apply fixed. Nothing seems to break (a miracle?) --- helm/gTopLevel/primitiveTactics.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/gTopLevel/primitiveTactics.ml b/helm/gTopLevel/primitiveTactics.ml index 8491155ad..8b3f025aa 100644 --- a/helm/gTopLevel/primitiveTactics.ml +++ b/helm/gTopLevel/primitiveTactics.ml @@ -258,7 +258,7 @@ let apply_tac ~term ~status:(proof, goal) = C.MutConstruct (uri,tyno,consno,exp_named_subst') | _ -> [],newmeta,[],term in - let metasenv' = newmetasenvfragment@metasenv in + let metasenv' = metasenv@newmetasenvfragment in prerr_endline ("^^^^^TERM': " ^ CicPp.ppterm term') ; let termty = CicSubstitution.subst_vars exp_named_subst_diff @@ -269,7 +269,7 @@ prerr_endline ("^^^^^TERMTY: " ^ CicPp.ppterm termty) ; let (consthead,newmetas,arguments,_) = new_metasenv_for_apply newmeta' proof context termty in - let newmetasenv = newmetas@metasenv' in + let newmetasenv = metasenv'@newmetas in let subst,newmetasenv' = CicUnification.fo_unif newmetasenv context consthead ty in -- 2.39.2