From f54d0b3158bc69a11fe579289f06f164ff5ccb94 Mon Sep 17 00:00:00 2001
From: jforest
Date: Wed, 25 Mar 2015 10:27:13 +0100
Subject: Correcting a bug introduced by universes polymorphism

---
 plugins/funind/functional_principles_types.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index d4f49af4de..deaf603ef0 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -274,10 +274,11 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro
   in
   let hook = Lemmas.mk_hook (hook new_principle_type) in
   begin
+    let evd,_ = Typing.e_type_of ~refresh:true (Global.env ()) Evd.empty new_principle_type in
     Lemmas.start_proof
       new_princ_name
       (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem))
-      (*FIXME*) Evd.empty
+      evd
     new_principle_type
       hook
     ;
@@ -323,7 +324,7 @@ let generate_functional_principle
 	let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
 	let value = change_property_sort s new_principle_type new_princ_name in
 	(*       Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
-	let ce = Declare.definition_entry value in (*FIXME, no poly, nothing *)
+	let ce = Declare.definition_entry value in 
 	ignore(
 	  Declare.declare_constant
 	    name
-- 
cgit v1.2.3