Merge branch 'v8.5'

4 files changed, 13 insertions, 9 deletions

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 45e5aaf545..a2bbf97ae3 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -604,7 +604,8 @@ let build_scheme fas =
 	      try
 		Smartlocate.global_with_alias f
 	      with Not_found ->
-	      	Errors.error ("Cannot find "^ Libnames.string_of_reference f)
+                errorlabstrm "FunInd.build_scheme"
+                  (str "Cannot find " ++ Libnames.pr_reference f)
 	    in
 	    let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in
 	    let evd',_ = Typing.e_type_of ~refresh:true (Global.env ()) evd' f in 
@@ -636,10 +637,12 @@ let build_case_scheme fa =
 (*   let id_to_constr id =  *)
 (*     Constrintern.global_reference  id *)
 (*   in  *)
-  let funs =  (fun (_,f,_) ->
-		 try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f))
-		 with Not_found ->
-		   Errors.error ("Cannot find "^ Libnames.string_of_reference f)) fa in
+  let funs =
+    let (_,f,_) = fa in
+    try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f))
+    with Not_found ->
+      errorlabstrm "FunInd.build_case_scheme"
+        (str "Cannot find " ++ Libnames.pr_reference f) in
   let first_fun,u = destConst  funs in
   let funs_mp,funs_dp,_ = Names.repr_con first_fun in
   let first_fun_kn = try fst (find_Function_infos  first_fun).graph_ind with Not_found -> raise No_graph_found in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 738ade8ca3..1c409500ef 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -109,7 +109,9 @@ let const_of_id id =
     qualid_of_reference (Libnames.Ident (Loc.ghost,id))
   in
   try Constrintern.locate_reference princ_ref
-  with Not_found -> Errors.error ("cannot find "^ Id.to_string id)
+  with Not_found ->
+    Errors.errorlabstrm "IndFun.const_of_id"
+      (str "cannot find " ++ Nameops.pr_id id)
 
 let def_of_const t =
    match (Term.kind_of_term t) with
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index d9ae87ecc1..d10924f886 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -378,7 +378,6 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	    observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres)));
 	    (* Conclusion *)
 	    observe_tac "exact" (fun g ->
-				 Pp.msgnl (str "TITI " ++ pf_apply Printer.pr_lconstr_env g (app_constructor g));
 				 Proofview.V82.of_tactic (exact_check (app_constructor g)) g)  
 	  ]
       )
@@ -427,7 +426,6 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
       in
       (params_bindings@lemmas_bindings)
     in
-    Pp.msgnl (str "princ_type := " ++ pf_apply Printer.pr_lconstr_env g princ_type);
     tclTHENSEQ
       [ 
 	observe_tac "principle" (Proofview.V82.of_tactic (assert_by
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index c6fab43d1c..77a7f006b7 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -305,7 +305,8 @@ let check_not_nested forbidden e =
       | Rel _ -> ()
       | Var x ->
         if Id.List.mem x forbidden
-        then error ("check_not_nested : failure "^Id.to_string x)
+        then errorlabstrm "Recdef.check_not_nested"
+               (str "check_not_nested: failure " ++ pr_id x)
       | Meta _ | Evar _ | Sort _ -> ()
       | Cast(e,_,t) -> check_not_nested e;check_not_nested t
       | Prod(_,t,b) -> check_not_nested t;check_not_nested b