Removing the compatibility layer from Leminv. Also removed an undocumented

variant of the Derive Inversion command which took the current goal as the
targeted inductive. It was unused in the contribs and it seemed rather
bad from the STM point of view, as it generated a lemma inside a proof.

3 files changed, 6 insertions, 31 deletions

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 1fbe5c4823..f8790796d0 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -359,12 +359,6 @@ open Leminv
 let seff id = Vernacexpr.VtSideff [id], Vernacexpr.VtLater
 
 VERNAC COMMAND EXTEND DeriveInversionClear
-  [ "Derive" "Inversion_clear" ident(na) hyp(id) ] => [ seff na ]
-  -> [ inversion_lemma_from_goal 1 na id Term.prop_sort false inv_clear_tac ]
-
-| [ "Derive" "Inversion_clear" natural(n) ident(na) hyp(id) ] => [ seff na ]
-  -> [ inversion_lemma_from_goal n na id Term.prop_sort false inv_clear_tac ]
-
 | [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort(s) ]
   => [ seff na ]
   -> [ add_inversion_lemma_exn na c s false inv_clear_tac ]
@@ -382,12 +376,6 @@ VERNAC COMMAND EXTEND DeriveInversion
 
 | [ "Derive" "Inversion" ident(na) "with" constr(c) ] => [ seff na ]
   -> [ add_inversion_lemma_exn na c GProp false inv_tac ]
-
-| [ "Derive" "Inversion" ident(na) hyp(id) ] => [ seff na ]
-  -> [ inversion_lemma_from_goal 1 na id Term.prop_sort false inv_tac ]
-
-| [ "Derive" "Inversion" natural(n) ident(na) hyp(id) ] => [ seff na ]
-  -> [ inversion_lemma_from_goal n na id Term.prop_sort false inv_tac ]
 END
 
 VERNAC COMMAND EXTEND DeriveDependentInversion
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 724cea5b72..2e55869de4 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -21,11 +21,11 @@ open Reductionops
 open Entries
 open Inductiveops
 open Environ
-open Tacmach
+open Tacmach.New
 open Pfedit
 open Clenv
 open Declare
-open Tacticals
+open Tacticals.New
 open Tactics
 open Decl_kinds
 
@@ -198,7 +198,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   let pf = Proof.start Evd.empty [invEnv,invGoal] in
   let pf =
     fst (Proof.run_tactic env (
-      Tacticals.New.tclTHEN intro (Tacticals.New.onLastHypId inv_op)) pf)
+      tclTHEN intro (onLastHypId inv_op)) pf)
   in
   let pfterm = List.hd (Proof.partial_proof pf) in
   let global_named_context = Global.named_context () in
@@ -243,16 +243,6 @@ let add_inversion_lemma name env sigma t sort dep inv_op =
 (* inv_op = Inv (derives de complete inv. lemma)
  * inv_op = InvNoThining (derives de semi inversion lemma) *)
 
-let inversion_lemma_from_goal n na (loc,id) sort dep_option inv_op =
-  let pts = get_pftreestate() in
-  let { it=gls ; sigma=sigma; } = Proof.V82.subgoals pts in
-  let gl = { it = List.nth gls (n-1) ; sigma=sigma; } in
-  let t =
-    try pf_get_hyp_typ gl id
-    with Not_found -> Pretype_errors.error_var_not_found_loc loc id in
-  let env = pf_env gl and sigma = project gl in
-  add_inversion_lemma na env sigma t sort dep_option inv_op
-
 let add_inversion_lemma_exn na com comsort bool tac =
   let env = Global.env () and sigma = Evd.empty in
   let c = Constrintern.interp_type sigma env com in
@@ -285,16 +275,16 @@ let lemInv_gen id c = try_intros_until (fun id -> Proofview.V82.tactic (lemInv i
 
 let lemInvIn id c ids =
   Proofview.Goal.enter begin fun gl ->
-    let hyps = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) ids in
+    let hyps = List.map (fun id -> pf_get_hyp id gl) ids in
     let intros_replace_ids =
       let concl = Proofview.Goal.concl gl in
       let nb_of_new_hyp  = nb_prod concl - List.length ids in
       if nb_of_new_hyp < 1  then
         intros_replacing ids
       else
-        (Tacticals.New.tclTHEN (Tacticals.New.tclDO nb_of_new_hyp intro) (intros_replacing ids))
+        (tclTHEN (tclDO nb_of_new_hyp intro) (intros_replacing ids))
     in
-    ((Tacticals.New.tclTHEN (Tacticals.New.tclTHEN (bring_hyps hyps) (Proofview.V82.tactic (lemInv id c)))
+    ((tclTHEN (tclTHEN (bring_hyps hyps) (Proofview.V82.tactic (lemInv id c)))
         (intros_replace_ids)))
   end
 
diff --git a/tactics/leminv.mli b/tactics/leminv.mli
index 36aa5e67f2..76223abedf 100644
--- a/tactics/leminv.mli
+++ b/tactics/leminv.mli
@@ -18,9 +18,6 @@ val lemInvIn_gen : quantified_hypothesis -> constr -> Id.t list -> unit Proofvie
 val lemInv_clause :
   quantified_hypothesis -> constr -> Id.t list -> unit Proofview.tactic
 
-val inversion_lemma_from_goal :
-  int -> Id.t -> Id.t located -> sorts -> bool ->
-    (Id.t -> unit Proofview.tactic) -> unit
 val add_inversion_lemma_exn :
   Id.t -> constr_expr -> glob_sort -> bool -> (Id.t -> unit Proofview.tactic) ->
     unit