diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-12 16:58:37 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-12 16:59:53 +0200 |
| commit | e4aa9817115b3d27eb7fca8fed86ffe397b868ad (patch) | |
| tree | efa8a3250bffa0a6fd7ac7d8c0f07ee17bc53734 /proofs/clenvtac.ml | |
| parent | 5dc8187aa8e6b481338035a022fec4025a25eb33 (diff) | |
While we don't have a clean alternative to Clenvtac, add a primitive
for tclEVARS which might solve existing goals.
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 94731b039..99ea2300c 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.tclEVARS evd' + Proofview.V82.tclEVARSADVANCE evd' with e when Errors.noncritical e -> (** This is Tacticals.tclFAIL *) Proofview.tclZERO (FailError (0, lazy (Errors.print e))) |