diff options
| -rw-r--r-- | tactics/extratactics.ml4 | 12 | ||||
| -rw-r--r-- | tactics/leminv.ml | 22 | ||||
| -rw-r--r-- | tactics/leminv.mli | 3 |
3 files changed, 6 insertions, 31 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 1fbe5c482..f8790796d 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 724cea5b7..2e55869de 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 36aa5e67f..76223abed 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 |