From c2855a3387be134d1220f301574b743572a94239 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Thu, 10 Nov 2016 11:39:27 +0100
Subject: Unification API using EConstr.

---
 pretyping/inductiveops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/inductiveops.ml')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index a93f2846b..e30ba21fd 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -504,7 +504,7 @@ let is_predicate_explicitly_dep env sigma pred arsign =
     let pv' = EConstr.of_constr (whd_all env sigma pval) in
     match EConstr.kind sigma pv', arsign with
       | Lambda (na,t,b), (LocalAssum _)::arsign ->
-	  srec (push_rel_assum (na, EConstr.Unsafe.to_constr t) env) b arsign
+	  srec (push_rel_assum (na, t) env) b arsign
       | Lambda (na,_,t), _ ->
 
        (* The following code has an impact on the introduction names
-- 
cgit v1.2.3