diff options
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 bc5f17bf5..5b9322bfe 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -95,7 +95,7 @@ let clenv_refine with_evars ?(with_classes=true) clenv = let clenv = { clenv with evd = evd' } in tclTHEN (tclEVARS (Evd.clear_metas evd')) - (refine_no_check (clenv_cast_meta clenv (clenv_value clenv))) gl + (refine_no_check (EConstr.of_constr (clenv_cast_meta clenv (clenv_value clenv)))) gl end open Unification |