Order of the generated metavariables for apply fixed. Nothing seems to

break (a miracle?)

diff --git a/helm/gTopLevel/primitiveTactics.ml b/helm/gTopLevel/primitiveTactics.ml
index 8491155ad8ed5d623a10b88378fd97d010e46d47..8b3f025aa07a575e9e9015528010d725b9bee5f7 100644 (file)
--- 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