* ElimSimplIntros replace by ElimIntrosSimpl. Simplification is performed

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

diff --git a/helm/gTopLevel/variousTactics.ml b/helm/gTopLevel/variousTactics.ml
index fc6897bafc9d8afa548a4bd5722705da0c6c0f0e..8f2dbce6ed8d03ffe5a1dac58f9a6f0eca5d1705 100644 (file)
--- a/helm/gTopLevel/variousTactics.ml
+++ b/helm/gTopLevel/variousTactics.ml
@@ -159,18 +159,10 @@ let elim_type_tac ~term ~status =
   let module T = Tacticals in
    T.thens 
     ~start: (P.cut_tac ~term) 
-    ~continuations:[ P.elim_simpl_intros_tac ~term:(C.Rel 1) ; T.id_tac ]
+    ~continuations:[ P.elim_intros_simpl_tac ~term:(C.Rel 1) ; T.id_tac ]
     ~status
 ;;
 
-(* Questa era gia' in ring.ml!!!! NB: adesso in ring non c'e' piu' :-) 
-let elim_type_tac ~term ~status =
-  warn "in Ring.elim_type_tac";
-  Tacticals.thens ~start:(cut_tac ~term)
-   ~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; Tacticals.id_tac] ~status
-*)
-
-
 let absurd_tac ~term ~status:((proof,goal) as status) =
   let module C = Cic in
   let module U = UriManager in
@@ -335,7 +327,7 @@ let decompose_tac ~clist ~status =
         if (term == C.Implicit)
          then raise (ProofEngineTypes.Fail "Decompose: nothing to decompose or no application")
          else T.then_
-                 ~start:(P.elim_simpl_intros_tac ~term)
+                 ~start:(P.elim_intros_simpl_tac ~term)
                  ~continuation:(S.clear ~hyp:(Some ((C.Name "FOO") , (C.Decl ty))))                (* ma che ipotesi sto cancellando??? *)  
                  ~status   
      in