diff options
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 2 | ||||
| -rw-r--r-- | printing/printer.ml | 3 | ||||
| -rw-r--r-- | proofs/logic.ml | 20 | ||||
| -rw-r--r-- | proofs/proof_type.ml | 1 | ||||
| -rw-r--r-- | proofs/proof_type.mli | 1 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 5 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 2 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 2 |
8 files changed, 2 insertions, 34 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 8e6bbcefd..d7344d355 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -589,7 +589,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = Proofview.V82.of_tactic (intro_using heq_id); onLastHypId (fun heq_id -> tclTHENLIST [ (* Then the new hypothesis *) - tclMAP introduction_no_check dyn_infos.rec_hyps; + tclMAP (fun id -> Proofview.V82.of_tactic (introduction ~check:false id)) dyn_infos.rec_hyps; observe_tac "after_introduction" (fun g' -> (* We get infos on the equations introduced*) let new_term_value_eq = pf_type_of g' (mkVar heq_id) in diff --git a/printing/printer.ml b/printing/printer.ml index 5b88e8c98..af81e192d 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -652,9 +652,6 @@ let pr_goal_by_id id = (* Elementary tactics *) let pr_prim_rule = function - | Intro id -> - str"intro " ++ pr_id id - | Cut (b,replace,id,t) -> if b then (* TODO: express "replace" *) diff --git a/proofs/logic.ml b/proofs/logic.ml index aa99dd036..b7a33cdba 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -522,26 +522,6 @@ let prim_refiner r sigma goal = in match r with (* Logical rules *) - | Intro id -> - if !check && mem_named_context id (named_context_of_val sign) then - error ("Variable " ^ Id.to_string id ^ " is already declared."); - (match kind_of_term (strip_outer_cast cl) with - | Prod (_,c1,b) -> - let (sg,ev,sigma) = mk_goal (push_named_context_val (id,None,c1) sign) - (subst1 (mkVar id) b) in - let sigma = - Goal.V82.partial_solution_to sigma goal sg (mkNamedLambda id c1 ev) in - ([sg], sigma) - | LetIn (_,c1,t1,b) -> - let (sg,ev,sigma) = - mk_goal (push_named_context_val (id,Some c1,t1) sign) - (subst1 (mkVar id) b) in - let sigma = - Goal.V82.partial_solution_to sigma goal sg (mkNamedLetIn id c1 t1 ev) in - ([sg], sigma) - | _ -> - raise (RefinerError IntroNeedsProduct)) - | Cut (b,replace,id,t) -> (* if !check && not (Retyping.get_sort_of env sigma t) then*) let (sg1,ev1,sigma) = mk_goal sign (nf_betaiota sigma t) in diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index d7e1c7b53..613f85a73 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -27,7 +27,6 @@ type goal = Goal.goal type tactic = goal sigma -> goal list sigma type prim_rule = - | Intro of Id.t | Cut of bool * bool * Id.t * types | FixRule of Id.t * int * (Id.t * int * constr) list * int | Cofix of Id.t * (Id.t * constr) list * int diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 2225a6e30..9361d48e6 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -19,7 +19,6 @@ open Misctypes is used by [Proof_tree] and [Refiner] *) type prim_rule = - | Intro of Id.t | Cut of bool * bool * Id.t * types | FixRule of Id.t * int * (Id.t * int * constr) list * int | Cofix of Id.t * (Id.t * constr) list * int diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 5b3605224..03f2fd2b4 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -105,10 +105,6 @@ let pf_matches = pf_apply ConstrMatching.matches_conv let refiner = refiner -(* This does not check that the variable name is not here *) -let introduction_no_check id = - refiner (Intro id) - let internal_cut_no_check replace id t gl = refiner (Cut (true,replace,id,t)) gl @@ -133,7 +129,6 @@ let mutual_cofix f others j gl = (* Versions with consistency checks *) -let introduction id = with_check (introduction_no_check id) let internal_cut b d t = with_check (internal_cut_no_check b d t) let internal_cut_rev b d t = with_check (internal_cut_rev_no_check b d t) let refine c = with_check (refine_no_check c) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index a9f7bffbf..8b95ae427 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -84,7 +84,6 @@ val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool (** {6 The most primitive tactics. } *) val refiner : rule -> tactic -val introduction_no_check : Id.t -> tactic val internal_cut_no_check : bool -> Id.t -> types -> tactic val refine_no_check : constr -> tactic val thin_no_check : Id.t list -> tactic @@ -94,7 +93,6 @@ val mutual_cofix : Id.t -> (Id.t * constr) list -> int -> tactic (** {6 The most primitive tactics with consistency and type checking } *) -val introduction : Id.t -> tactic val internal_cut : bool -> Id.t -> types -> tactic val internal_cut_rev : bool -> Id.t -> types -> tactic val refine : constr -> tactic diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index d048d5bcd..0c0204081 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -726,7 +726,7 @@ let case_eq_intros_rewrite x = let h = Tacmach.New.of_old (fun g -> fresh_id hyps (Id.of_string "heq") g) gl in Tacticals.New.tclTHENLIST [ Tacticals.New.tclDO (n'-n-1) intro; - Proofview.V82.tactic (Tacmach.introduction h); + introduction h; rewrite_except h] end ] |