diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-31 19:26:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-31 19:26:40 +0200 |
| commit | 68191dcce820a8135a84e716bddb7cf78476c360 (patch) | |
| tree | 2eb6ccd65aaeef11d99bd367edb4b4ed1fd94169 /proofs/refiner.mli | |
| parent | e3eedfd7b585f2ab71c6c5750dcefa4d8ecb6f38 (diff) | |
Removing the Change_evar refiner rule.
Diffstat (limited to 'proofs/refiner.mli')
| -rw-r--r-- | proofs/refiner.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/proofs/refiner.mli b/proofs/refiner.mli index db2c081d1..012209410 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 |