* ElimSimplIntros replace by ElimIntrosSimpl. Simplification is performed

[helm.git] / helm / gTopLevel / primitiveTactics.ml

diff --git a/helm/gTopLevel/primitiveTactics.ml b/helm/gTopLevel/primitiveTactics.ml
index 9a037d754d8acc3c37adbc830c41f90c382143fa..ccd8ccfe0ad63eddcd5c572092a78fd11d2ece72 100644 (file)
--- a/helm/gTopLevel/primitiveTactics.ml
+++ b/helm/gTopLevel/primitiveTactics.ml
@@ -500,15 +500,16 @@ da subst1!!!! Dovrei rimuoverle o sono innocue?*)
                       List.map (function (i,_,_) -> i) new_uninstantiatedmetas)
 ;;
 
-let elim_simpl_intros_tac ~term =
+(* The simplification is performed only on the conclusion *)
+let elim_intros_simpl_tac ~term =
  Tacticals.then_ ~start:(elim_tac ~term)
   ~continuation:
-   (Tacticals.then_
-     ~start:(ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None)
-     ~continuation:intros_tac)
+   (Tacticals.thens
+     ~start:intros_tac
+     ~continuations:
+       [ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None])
 ;;
 
-
 exception NotConvertible
 
 (*CSC: Bug (or feature?). [with_what] is parsed in the context of the goal,  *)