From 81cc12ae4ebd9741585b38f41c7fb5eb6c5ae916 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 9 Dec 2002 10:53:29 +0000
Subject: [PATCH] * ElimSimplIntros replace by ElimIntrosSimpl. Simplification
 is performed   only in the conclusion and not (yet) on the hypothesis.

---
 helm/gTopLevel/primitiveTactics.ml  | 11 ++++++-----
 helm/gTopLevel/primitiveTactics.mli |  2 +-
 helm/gTopLevel/proofEngine.ml       |  4 ++--
 helm/gTopLevel/proofEngine.mli      |  2 +-
 helm/gTopLevel/variousTactics.ml    | 12 ++----------
 5 files changed, 12 insertions(+), 19 deletions(-)

diff --git a/helm/gTopLevel/primitiveTactics.ml b/helm/gTopLevel/primitiveTactics.ml
index 9a037d754..ccd8ccfe0 100644
--- 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,  *)
diff --git a/helm/gTopLevel/primitiveTactics.mli b/helm/gTopLevel/primitiveTactics.mli
index 59a714c78..dad385339 100644
--- a/helm/gTopLevel/primitiveTactics.mli
+++ b/helm/gTopLevel/primitiveTactics.mli
@@ -34,7 +34,7 @@ val cut_tac:
 val letin_tac:
   term: Cic.term -> ProofEngineTypes.tactic 
 
-val elim_simpl_intros_tac:
+val elim_intros_simpl_tac:
   term: Cic.term -> ProofEngineTypes.tactic 
 
 val change_tac:
diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 7b4c68ab5..81b2cd3e0 100644
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -169,8 +169,8 @@ let intros () = apply_tactic PrimitiveTactics.intros_tac
 let cut term = apply_tactic (PrimitiveTactics.cut_tac ~term)
 let letin term = apply_tactic (PrimitiveTactics.letin_tac ~term)
 let exact term = apply_tactic (PrimitiveTactics.exact_tac ~term)
-let elim_simpl_intros term =
-  apply_tactic (PrimitiveTactics.elim_simpl_intros_tac ~term)
+let elim_intros_simpl term =
+  apply_tactic (PrimitiveTactics.elim_intros_simpl_tac ~term)
 let change ~goal_input:what ~input:with_what =
   apply_tactic (PrimitiveTactics.change_tac ~what ~with_what)
 
diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli
index 73dcb4d75..b53e3022d 100644
--- a/helm/gTopLevel/proofEngine.mli
+++ b/helm/gTopLevel/proofEngine.mli
@@ -50,7 +50,7 @@ val intros : unit -> unit
 val cut : Cic.term -> unit
 val letin : Cic.term -> unit
 val exact : Cic.term -> unit
-val elim_simpl_intros : Cic.term -> unit
+val elim_intros_simpl : Cic.term -> unit
 val change : goal_input:Cic.term -> input:Cic.term -> unit
 
   (* structural tactics *)
diff --git a/helm/gTopLevel/variousTactics.ml b/helm/gTopLevel/variousTactics.ml
index fc6897baf..8f2dbce6e 100644
--- 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
-- 
2.39.2