From 85ab3e298aa1d7333787c1fa44d25df189ac255c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 8 Nov 2016 19:02:40 +0100
Subject: Pretyping API using EConstr.

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

(limited to 'plugins/decl_mode/decl_interp.ml')

diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 65d273fafb..ddf0137354 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -173,7 +173,7 @@ let get_eq_typ info env =
     typ
 
 let interp_constr_in_type typ env sigma c =
-  fst (understand env sigma (fst c) ~expected_type:(OfType typ))(*FIXME*)
+  fst (understand env sigma (fst c) ~expected_type:(OfType (EConstr.of_constr typ)))(*FIXME*)
 
 let interp_statement interp_it env sigma st =
   {st_label=st.st_label;
-- 
cgit v1.2.3