From cbea91d815f134d63d02d8fb1bd78ed97db28cd1 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 11 Nov 2016 19:52:48 +0100 Subject: Tacmach API using EConstr. --- proofs/clenvtac.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'proofs/clenvtac.ml') 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 -- cgit v1.2.3