Merge PR #244.

8 files changed, 35 insertions, 35 deletions

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 234c3e75ec..cc699e5d3d 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -611,7 +611,7 @@ let build_scheme fas =
 	      try
 		Smartlocate.global_with_alias f
 	      with Not_found ->
-                errorlabstrm "FunInd.build_scheme"
+                user_err ~hdr:"FunInd.build_scheme"
                   (str "Cannot find " ++ Libnames.pr_reference f)
 	    in
 	    let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in
@@ -645,7 +645,7 @@ let build_case_scheme fa =
     let (_,f,_) = fa in
     try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f))
     with Not_found ->
-      errorlabstrm "FunInd.build_case_scheme"
+      user_err ~hdr:"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
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 4d02c77c82..de2e5ea4e2 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -631,7 +631,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	let (ind,_) =
 	  try Inductiveops.find_inductive env (Evd.from_env env) b_typ
 	  with Not_found ->
-	    errorlabstrm "" (str "Cannot find the inductive associated to " ++
+	    user_err  (str "Cannot find the inductive associated to " ++
 			       Printer.pr_glob_constr b ++ str " in " ++
 			       Printer.pr_glob_constr rt ++ str ". try again with a cast")
 	in
@@ -663,7 +663,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	  let (ind,_) =
 	    try Inductiveops.find_inductive env (Evd.from_env env) b_typ
 	    with Not_found ->
-	      errorlabstrm "" (str "Cannot find the inductive associated to " ++
+	      user_err  (str "Cannot find the inductive associated to " ++
 				 Printer.pr_glob_constr b ++ str " in " ++
 				 Printer.pr_glob_constr rt ++ str ". try again with a cast")
 	  in
@@ -1198,7 +1198,7 @@ let rec compute_cst_params relnames params = function
   | GSort _ -> params
   | GHole _ -> params
   | GIf _ | GRec _ | GCast _ ->
-      raise (UserError("compute_cst_params", str "Not handled case"))
+      raise (UserError(Some "compute_cst_params", str "Not handled case"))
 and compute_cst_params_from_app acc (params,rtl) =
   match params,rtl with
     | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *)
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 01e5ef7fba..4e561fc7e5 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -406,7 +406,7 @@ let is_free_in id =
 
     | GIf(_,cond,_,br1,br2) ->
 	is_free_in cond || is_free_in br1 || is_free_in br2
-    | GRec _ -> raise (UserError("",str "Not handled GRec"))
+    | GRec _ -> raise (UserError(None,str "Not handled GRec"))
     | GSort _ -> false
     | GHole _ -> false
     | GCast (_,b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t
@@ -502,7 +502,7 @@ let replace_var_by_term x_id term =
 	      replace_var_by_pattern lhs,
 	      replace_var_by_pattern rhs
 	     )
-      | GRec _ -> raise (UserError("",str "Not handled GRec"))
+      | GRec _ -> raise (UserError(None,str "Not handled GRec"))
       | GSort _ -> rt
       | GHole _ -> rt
       | GCast(loc,b,c) ->
@@ -655,7 +655,7 @@ let zeta_normalize =
 	      zeta_normalize_term lhs,
 	      zeta_normalize_term rhs
 	     )
-      | GRec _ -> raise (UserError("",str "Not handled GRec"))
+      | GRec _ -> raise (UserError(None,str "Not handled GRec"))
       | GSort _ -> rt
       | GHole _ -> rt
       | GCast(loc,b,c) ->
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 51cf7f4f49..99b04898ba 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -43,7 +43,7 @@ let functional_induction with_clean c princl pat =
 		let finfo = (* we first try to find out a graph on f *)
 		  try find_Function_infos c'
 		  with Not_found ->
-		    errorlabstrm "" (str "Cannot find induction information on "++
+		    user_err  (str "Cannot find induction information on "++
 				       Printer.pr_lconstr (mkConst c') )
 		in
 		match Tacticals.elimination_sort_of_goal g with
@@ -71,11 +71,11 @@ let functional_induction with_clean c princl pat =
 		    (b,a)
 		    (* mkConst(const_of_id princ_name ),g (\* FIXME *\) *)
 		  with Not_found -> (* This one is neither defined ! *)
-		    errorlabstrm "" (str "Cannot find induction principle for "
+		    user_err  (str "Cannot find induction principle for "
 				     ++Printer.pr_lconstr (mkConst c') )
 	      in
 	      (princ,NoBindings, Tacmach.pf_unsafe_type_of g' princ,g')
-	   | _ -> raise (UserError("",str "functional induction must be used with a function" ))
+	   | _ -> raise (UserError(None,str "functional induction must be used with a function" ))
 	 end
       | Some ((princ,binding)) ->
 	 princ,binding,Tacmach.pf_unsafe_type_of g princ,g
@@ -176,7 +176,7 @@ let build_newrecursive l =
        match body_opt with 
 	 | Some body -> 
 	     (fixna,bll,ar,body)
-	 | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given")
+	 | None -> user_err ~hdr:"Function" (str "Body of Function must be given")
     ) l
   in
   build_newrecursive l'
@@ -322,7 +322,7 @@ let error_error names e =
   in
   match e with
     | Building_graph e ->
-	errorlabstrm ""
+	user_err 
 	  (str "Cannot define graph(s) for " ++
 	     h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
 	     e_explain e)
@@ -392,7 +392,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
 let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
   match fixpoint_exprl with
     | [(((_,fname),pl),_,bl,ret_type,body),_] when not is_rec ->
-      let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in 
+      let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in 
       Command.do_definition
 	fname
 	(Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl
@@ -631,7 +631,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
 	      | _ -> assert false
 	  in 
 	  let fixpoint_exprl = [fixpoint_expr] in 
-	  let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in 
+	  let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in 
 	  let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
 	  let using_lemmas = [] in 
 	  let pre_hook pconstants =
@@ -657,7 +657,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
 	  let fixpoint_exprl = [fixpoint_expr] in 
 	  let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
 	  let using_lemmas = [] in
-	  let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in 
+	  let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in 
 	  let pre_hook pconstants =
 	    generate_principle
 	      (ref (Evd.from_env (Global.env ())))
@@ -835,9 +835,9 @@ let make_graph (f_ref:global_reference) =
       | ConstRef c ->
 	  begin try c,Global.lookup_constant c
 	  with Not_found ->
-	    raise (UserError ("",str "Cannot find " ++ Printer.pr_lconstr (mkConst c)) )
+	    raise (UserError (None,str "Cannot find " ++ Printer.pr_lconstr (mkConst c)) )
 	  end
-      | _ -> raise (UserError ("", str "Not a function reference") )
+      | _ -> raise (UserError (None, str "Not a function reference") )
   in
   (match Global.body_of_constant_body c_body with
      | None -> error "Cannot build a graph over an axiom !"
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index f56e92414e..a45effb167 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -49,7 +49,7 @@ let locate_constant ref =
 
 let locate_with_msg msg f x =
   try f x
-  with Not_found -> raise (CErrors.UserError("", msg))
+  with Not_found -> raise (CErrors.UserError(None, msg))
 
 
 let filter_map filter f =
@@ -73,7 +73,7 @@ let chop_rlambda_n  =
 	  | Glob_term.GLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b
 	  | Glob_term.GLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b
 	  | _ ->
-	      raise (CErrors.UserError("chop_rlambda_n",
+	      raise (CErrors.UserError(Some "chop_rlambda_n",
 				    str "chop_rlambda_n: Not enough Lambdas"))
   in
   chop_lambda_n []
@@ -85,7 +85,7 @@ let chop_rprod_n  =
       else
 	match rt with
 	  | Glob_term.GProd(_,name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b
-	  | _ -> raise (CErrors.UserError("chop_rprod_n",str "chop_rprod_n: Not enough products"))
+	  | _ -> raise (CErrors.UserError(Some "chop_rprod_n",str "chop_rprod_n: Not enough products"))
   in
   chop_prod_n []
 
@@ -110,7 +110,7 @@ let const_of_id id =
   in
   try Constrintern.locate_reference princ_ref
   with Not_found ->
-    CErrors.errorlabstrm "IndFun.const_of_id"
+    CErrors.user_err ~hdr:"IndFun.const_of_id"
       (str "cannot find " ++ Nameops.pr_id id)
 
 let def_of_const t =
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 0178c44d09..c8b4e48337 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1000,7 +1000,7 @@ let invfun qhyp f  =
   let f =
     match f with
       | ConstRef f -> f
-      | _ -> raise (CErrors.UserError("",str "Not a function"))
+      | _ -> raise (CErrors.UserError(None,str "Not a function"))
   in
   try
     let finfos = find_Function_infos f in
@@ -1045,19 +1045,19 @@ let invfun qhyp f g =
 			 functional_inversion kn hid  f2 f_correct g
 		       with
 			 | Failure "" ->
-			     errorlabstrm "" (str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function")
+			     user_err  (str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function")
 			 | Option.IsNone  ->
 			     if do_observe ()
 			     then
 			       error "Cannot use equivalence with graph for any side of the equality"
-			     else errorlabstrm "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
+			     else user_err  (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
 			 | Not_found ->
 			     if do_observe ()
 			     then
 			       error "No graph found for any side of equality"
-			     else errorlabstrm "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
+			     else user_err  (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
 		   end
-	       | _ -> errorlabstrm "" (Ppconstr.pr_id hid ++ str " must be an equality ")
+	       | _ -> user_err  (Ppconstr.pr_id hid ++ str " must be an equality ")
 	  end)
 	  qhyp
           end
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 14550a9fc7..7cbe787c3b 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -903,7 +903,7 @@ let find_Function_infos_safe (id:Id.t): Indfun_common.function_info =
       locate_constant f_ref in
     try find_Function_infos (kn_of_id id)
     with Not_found ->
-      errorlabstrm "indfun" (Nameops.pr_id id ++ str " has no functional scheme")
+      user_err ~hdr:"indfun" (Nameops.pr_id id ++ str " has no functional scheme")
 
 (** [merge id1 id2 args1 args2 id] builds and declares a new inductive
     type called [id], representing the merged graphs of both graphs
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 65f96c8313..f43251bc50 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -307,7 +307,7 @@ let check_not_nested forbidden e =
       | Rel _ -> ()
       | Var x ->
         if Id.List.mem x forbidden
-        then errorlabstrm "Recdef.check_not_nested"
+        then user_err ~hdr:"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
@@ -327,7 +327,7 @@ let check_not_nested forbidden e =
   try 
     check_not_nested e 
   with UserError(_,p) -> 
-    errorlabstrm "_" (str "on expr : " ++ Printer.pr_lconstr e ++ str " " ++ p)
+    user_err ~hdr:"_" (str "on expr : " ++ Printer.pr_lconstr e ++ str " " ++ p)
 
 (* ['a info] contains the local information for traveling *)
 type 'a infos = 
@@ -442,7 +442,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) =
 	  check_not_nested (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
 	  jinfo.otherS () expr_info continuation_tac expr_info
 	with e when CErrors.noncritical e ->
-	  errorlabstrm "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id)
+	  user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id)
       end
     | Lambda(n,t,b) -> 
       begin
@@ -450,7 +450,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) =
 	  check_not_nested (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
 	  jinfo.otherS () expr_info continuation_tac expr_info
 	with e when CErrors.noncritical e ->
-	  errorlabstrm "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id)
+	  user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id)
       end
     | Case(ci,t,a,l) -> 
       begin
@@ -478,7 +478,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) =
 	      jinfo.apP (f,args) expr_info continuation_tac in 
 	    travel_args jinfo
 	      expr_info.is_main_branch new_continuation_tac new_infos
-	  | Case _ ->  errorlabstrm "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)")
+	  | Case _ ->  user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)")
 	  | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_lconstr expr_info.info)
       end
     | Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t}
@@ -723,8 +723,8 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
 	 (List.map_i (fun i e -> observe_tac (str "do treat case") (treat_case f_is_present to_thin_intro (next_step continuation_tac) ci.ci_cstr_ndecls.(i) e new_info)) 0 (Array.to_list l)
 	 ))
     with 
-      | UserError("Refiner.thensn_tac3",_) 
-      | UserError("Refiner.tclFAIL_s",_) ->
+      | UserError(Some "Refiner.thensn_tac3",_) 
+      | UserError(Some "Refiner.tclFAIL_s",_) ->
 	(observe_tac (str "is computable " ++ Printer.pr_lconstr new_info.info) (next_step continuation_tac {new_info with info = nf_betaiotazeta new_info.info} )
 	))
     g