Merge branch 'v8.5' into trunk

1 files changed, 21 insertions, 20 deletions

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 80167686aa..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
@@ -447,7 +448,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 +499,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)