From e27949240f5b1ee212e7d0fe3326a21a13c4abb0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 6 Nov 2016 17:21:44 +0100
Subject: Typing API using EConstr.

---
 ltac/tacinterp.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'ltac/tacinterp.ml')

diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 34faa028f2..8f5ac7e766 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -791,7 +791,7 @@ let interp_may_eval f ist env sigma = function
 	let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in
 	let evdref = ref sigma in
 	let c = subst_meta [Constr_matching.special_meta,ic] ctxt in
-	let c = Typing.e_solve_evars env evdref c in
+	let c = Typing.e_solve_evars env evdref (EConstr.of_constr c) in
 	!evdref , c
       with
 	| Not_found ->
@@ -799,7 +799,7 @@ let interp_may_eval f ist env sigma = function
 	    (str "Unbound context identifier" ++ pr_id s ++ str"."))
   | ConstrTypeOf c ->
       let (sigma,c_interp) = f ist env sigma c in
-      Typing.type_of ~refresh:true env sigma c_interp
+      Typing.type_of ~refresh:true env sigma (EConstr.of_constr c_interp)
   | ConstrTerm c ->
      try
 	f ist env sigma c
-- 
cgit v1.2.3