diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/refiner.ml | 2 | ||||
| -rw-r--r-- | proofs/refiner.mli | 1 |
2 files changed, 0 insertions, 3 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 6a0ba30bbf..ad84afd47e 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -271,5 +271,3 @@ let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t)) (* Change evars *) let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma} -let tclPUSHEVARUNIVCONTEXT ctx gl = - tclEVARS (Evd.merge_universe_context (project gl) ctx) gl diff --git a/proofs/refiner.mli b/proofs/refiner.mli index d4f2239a59..3471f38e9e 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -32,7 +32,6 @@ val tclIDTAC_MESSAGE : Pp.t -> tactic (** [tclEVARS sigma] changes the current evar map *) val tclEVARS : evar_map -> tactic -val tclPUSHEVARUNIVCONTEXT : UState.t -> tactic (** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies |