X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FprimitiveTactics.ml;h=8b3f025aa07a575e9e9015528010d725b9bee5f7;hb=347d3c4262af67b378f4a65f735f48797ffc37a3;hp=21d5d67c6fd8bcd4088a26571c64ee771ec2f757;hpb=3066e4dcb7270a5eb20020a91d45da9eb87e2f2e;p=helm.git

diff --git a/helm/gTopLevel/primitiveTactics.ml b/helm/gTopLevel/primitiveTactics.ml
index 21d5d67c6..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
@@ -278,7 +278,7 @@ prerr_endline ("^^^^^TERMTY: " ^ CicPp.ppterm termty) ;
         let old_uninstantiatedmetas,new_uninstantiatedmetas =
          (* subst_in doesn't need the context. Hence the underscore. *)
          let subst_in _ = CicUnification.apply_subst subst in
-          classify_metas newmeta' in_subst_domain subst_in newmetasenv'
+          classify_metas newmeta in_subst_domain subst_in newmetasenv'
         in
          let bo' =
           apply_subst
@@ -506,7 +506,8 @@ da subst1!!!! Dovrei rimuoverle o sono innocue?*)
 let elim_simpl_intros_tac ~term =
  Tacticals.then_ ~start:(elim_tac ~term)
   ~continuation:
-   (Tacticals.then_ ~start:ReductionTactics.simpl_tac
+   (Tacticals.then_
+     ~start:(ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None)
      ~continuation:(intros_tac ~name:"FOO"))
 ;;