Merge PR #244.

1 files changed, 7 insertions, 7 deletions

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 160b3bc3f..7da738508 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -41,7 +41,7 @@ exception Elimconst
 exception Redelimination
 
 let error_not_evaluable r =
-  errorlabstrm "error_not_evaluable"
+  user_err ~hdr:"error_not_evaluable"
     (str "Cannot coerce" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r ++
      spc () ++ str "to an evaluable reference.")
 
@@ -989,7 +989,7 @@ let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t ->
       incr pos;
       if ok then begin
         if Option.has_some nested then
-          errorlabstrm "" (str "The subterm at occurrence " ++ int (Option.get nested) ++ str " overlaps with the subterm at occurrence " ++ int (!pos-1) ++ str ".");
+          user_err  (str "The subterm at occurrence " ++ int (Option.get nested) ++ str " overlaps with the subterm at occurrence " ++ int (!pos-1) ++ str ".");
         (* Skip inner occurrences for stable counting of occurrences *)
         if locs != [] then
           ignore (traverse_below (Some (!pos-1)) envc t);
@@ -1155,13 +1155,13 @@ let pattern_occs loccs_trm = { e_redfun = begin fun env sigma c ->
 let check_privacy env ind =
   let spec = Inductive.lookup_mind_specif env (fst ind) in
   if Inductive.is_private spec then
-    errorlabstrm "" (str "case analysis on a private type.")
+    user_err  (str "case analysis on a private type.")
   else ind
 
 let check_not_primitive_record env ind =
   let spec = Inductive.lookup_mind_specif env (fst ind) in
     if Inductive.is_primitive_record spec then
-      errorlabstrm "" (str "case analysis on a primitive record type: " ++
+      user_err  (str "case analysis on a primitive record type: " ++
 		       str "use projections or let instead.")
     else ind
 
@@ -1178,14 +1178,14 @@ let reduce_to_ind_gen allow_product env sigma t =
 	  if allow_product then
 	    elimrec (push_rel (LocalAssum (n,ty)) env) t' ((LocalAssum (n,ty))::l)
 	  else
-	    errorlabstrm "" (str"Not an inductive definition.")
+	    user_err  (str"Not an inductive definition.")
       | _ ->
 	  (* Last chance: we allow to bypass the Opaque flag (as it
 	     was partially the case between V5.10 and V8.1 *)
 	  let t' = whd_all env sigma t in
 	  match kind_of_term (fst (decompose_app t')) with
 	    | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t' l)
-	    | _ -> errorlabstrm "" (str"Not an inductive product.")
+	    | _ -> user_err  (str"Not an inductive product.")
   in
   elimrec env t []
 
@@ -1235,7 +1235,7 @@ let one_step_reduce env sigma c =
   applist (redrec (c,[]))
 
 let error_cannot_recognize ref =
-  errorlabstrm ""
+  user_err 
     (str "Cannot recognize a statement based on " ++
      Nametab.pr_global_env Id.Set.empty ref ++ str".")