diff options
| author | Pierre-Marie Pédrot | 2014-03-31 19:26:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-03-31 19:26:40 +0200 |
| commit | 68191dcce820a8135a84e716bddb7cf78476c360 (patch) | |
| tree | 2eb6ccd65aaeef11d99bd367edb4b4ed1fd94169 /proofs | |
| parent | e3eedfd7b585f2ab71c6c5750dcefa4d8ecb6f38 (diff) | |
Removing the Change_evar refiner rule.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/logic.ml | 5 | ||||
| -rw-r--r-- | proofs/proof_type.ml | 1 | ||||
| -rw-r--r-- | proofs/proof_type.mli | 1 | ||||
| -rw-r--r-- | proofs/refiner.ml | 5 | ||||
| -rw-r--r-- | proofs/refiner.mli | 3 |
5 files changed, 0 insertions, 15 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index f283d0f339..30905e5771 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -713,8 +713,3 @@ let prim_refiner r sigma goal = let ev = Vars.replace_vars [(id2,mkVar id1)] ev in let sigma = Goal.V82.partial_solution sigma goal ev in ([gl], sigma) - - | Change_evars -> - (* Normalises evars in goals. Used by instantiate. *) - let (goal,sigma) = Goal.V82.nf_evar sigma goal in - ([goal],sigma) diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 3ee7c87f77..f98bfa5ea2 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -39,7 +39,6 @@ type prim_rule = | Move of bool * Id.t * Id.t move_location | Order of Id.t list | Rename of Id.t * Id.t - | Change_evars (** Nowadays, the only rules we'll consider are the primitive rules *) diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 85ecfdd8a2..a5d6940770 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -31,7 +31,6 @@ type prim_rule = | Move of bool * Id.t * Id.t move_location | Order of Id.t list | Rename of Id.t * Id.t - | Change_evars (** Nowadays, the only rules we'll consider are the primitive rules *) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 6094287927..7e80b40e52 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -27,8 +27,6 @@ let refiner pr goal_sigma = let (sgl,sigma') = prim_refiner pr goal_sigma.sigma goal_sigma.it in { it = sgl; sigma = sigma'; } -let norm_evar_tac gl = refiner (Change_evars) gl - (*********************) (* Tacticals *) (*********************) @@ -47,9 +45,6 @@ let apply_sig_tac r tac g = (* [goal_goal_list : goal sigma -> goal list sigma] *) let goal_goal_list gls = {it=[gls.it]; sigma=gls.sigma; } -(* forces propagation of evar constraints *) -let tclNORMEVAR = norm_evar_tac - (* identity tactic without any message *) let tclIDTAC gls = goal_goal_list gls diff --git a/proofs/refiner.mli b/proofs/refiner.mli index db2c081d1b..012209410a 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -27,9 +27,6 @@ val refiner : rule -> tactic (** {6 Tacticals. } *) -(** [tclNORMEVAR] forces propagation of evar constraints *) -val tclNORMEVAR : tactic - (** [tclIDTAC] is the identity tactic without message printing*) val tclIDTAC : tactic val tclIDTAC_MESSAGE : Pp.std_ppcmds -> tactic |