From 810454922d4eeffaf9f92ccd7d8e10a1433de947 Mon Sep 17 00:00:00 2001
From: forest
Date: Mon, 23 Mar 2015 14:54:18 +0100
Subject: correcting a bug with aliased when using Functional Scheme

---
 plugins/funind/functional_principles_types.ml | 36 +++++++++++++--------------
 1 file changed, 18 insertions(+), 18 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 80167686aa..d4f49af4de 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -447,7 +447,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
   let first_fun = List.hd funs in
 
 
-  let funs_mp,funs_dp,_ = Names.repr_con first_fun in
+  let funs_mp,funs_dp,_ = KerName.repr (Constant.canonical first_fun) in
   let first_fun_kn =
     try
       fst (find_Function_infos  first_fun).graph_ind
@@ -498,27 +498,27 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
 	0
 	(prove_princ_for_struct false 0 (Array.of_list funs))
 	(fun _ _ _ -> ())
-  with e when Errors.noncritical e ->
-    begin
-      begin
-	try
-	  let id = Pfedit.get_current_proof_name () in
-	  let s = Id.to_string id in
-	  let n = String.length "___________princ_________" in
-	  if String.length s >= n
-	  then if String.equal (String.sub s 0 n) "___________princ_________"
-	  then Pfedit.delete_current_proof ()
-	  else ()
-	  else ()
-	with e when Errors.noncritical e -> ()
-      end;
-      raise (Defining_principle e)
-    end
+    with e when Errors.noncritical e ->
+       begin
+	 begin
+	   try
+	     let id = Pfedit.get_current_proof_name () in
+	     let s = Id.to_string id in
+	     let n = String.length "___________princ_________" in
+	     if String.length s >= n
+	     then if String.equal (String.sub s 0 n) "___________princ_________"
+		  then Pfedit.delete_current_proof ()
+		  else ()
+	     else ()
+	   with e when Errors.noncritical e -> ()
+	 end;
+	 raise (Defining_principle e)
+       end
 
   in
   incr i;
   let opacity =
-    let finfos = find_Function_infos this_block_funs.(0) in
+    let finfos = find_Function_infos first_fun in
     try
       let equation =  Option.get finfos.equation_lemma in
       Declareops.is_opaque (Global.lookup_constant equation)
-- 
cgit v1.2.3


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