* ElimSimplIntros replace by ElimIntrosSimpl. Simplification is performed

  only in the conclusion and not (yet) on the hypothesis.

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,  *)

diff --git a/helm/gTopLevel/primitiveTactics.mli b/helm/gTopLevel/primitiveTactics.mli
index 59a714c78c938e3144f963a12390b54d332451f0..dad385339b876bbe4da402bf4d9068c62d9b3923 100644 (file)
--- 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 7b4c68ab54a9884e88baeae1acf4d970038348d8..81b2cd3e04540936f617433b26aed3b96ca36d8b 100644 (file)
--- 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 73dcb4d75c6c6b5a6b4777d4266faaff70813396..b53e3022d11cb0ffff7656b455fac848f2913e56 100644 (file)
--- 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 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