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.

---
 plugins/firstorder/instances.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/firstorder/instances.ml')

diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 44bdb585a1..6c245063c8 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -104,7 +104,7 @@ let mk_open_instance id idc gl m t=
   let evmap=Refiner.project gl in
   let var_id=
     if id==dummy_id then dummy_bvid else
-      let typ=pf_unsafe_type_of gl idc in
+      let typ=pf_unsafe_type_of gl (EConstr.of_constr idc) in
 	(* since we know we will get a product,
 	   reduction is not too expensive *)
       let (nam,_,_)=destProd (whd_all env evmap (EConstr.of_constr typ)) in
-- 
cgit v1.2.3