diff options
| author | Enrico Tassi | 2020-05-05 19:27:12 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2020-05-05 19:27:12 +0200 |
| commit | bc79d319d38f766a6b7bbeb1f1071b046642089b (patch) | |
| tree | 1f2f52d171b0694dfecf0f7003ae96630e5837ca /proofs/refiner.ml | |
| parent | f4532cf12ce96a6e60115641356582ff44ea525f (diff) | |
| parent | d87f8d10d089c3a33ddb36a71ab6fc082d0d1140 (diff) | |
Merge PR #12227: Spring cleaning of the tactic compatibility layer
Reviewed-by: gares
Diffstat (limited to 'proofs/refiner.ml')
| -rw-r--r-- | proofs/refiner.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 75c3436cf4..29a47c5acd 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -37,6 +37,8 @@ let refiner ~check = CProfile.profile2 refiner_key (refiner ~check) else refiner ~check +let refiner ~check c = Proofview.V82.tactic ~nf_evars:false (refiner ~check c) + (*********************) (* Tacticals *) (*********************) @@ -269,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 |