diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-17 15:31:58 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-22 07:31:44 +0200 |
| commit | cadfe23210c8edaab1f22d0edb7acc33fb9ff782 (patch) | |
| tree | 50a7a8942285cdbf9555122c0abfa03e493afec6 /proofs/clenvtac.ml | |
| parent | d76c6d9c92d8486ef4b672f9b44e5c6ea782d7ff (diff) | |
Proofview: split [V82] module into [Unsafe] and [V82].
The Unsafe module is for unsafe tactics which cannot be done without anytime soon. Whereas V82 indicates a function which we want to get rid of and that shouldn't be used in a new function.
Diffstat (limited to 'proofs/clenvtac.ml')
| -rw-r--r-- | proofs/clenvtac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 76fc37d37..7d25bb665 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -123,7 +123,7 @@ let unify ?(flags=fail_quick_unif_flags) m = let evd = create_goal_evar_defs (Proofview.Goal.sigma gl) in try let evd' = w_unify env evd CONV ~flags m n in - Proofview.V82.tclEVARSADVANCE evd' + Proofview.Unsafe.tclEVARSADVANCE evd' with e when Errors.noncritical e -> (** This is Tacticals.tclFAIL *) Proofview.tclZERO (FailError (0, lazy (Errors.print e))) |