Merge PR #244.

1 files changed, 7 insertions, 7 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index e12fe5d70a..5aba6b614f 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -153,7 +153,7 @@ let reorder_context env sign ord =
       | top::ord' when mem_q top moved_hyps ->
           let ((d,h),mh) = find_q top moved_hyps in
           if occur_vars_in_decl env h d then
-            errorlabstrm "reorder_context"
+            user_err ~hdr:"reorder_context"
               (str "Cannot move declaration " ++ pr_id top ++ spc() ++
               str "before " ++
               pr_sequence pr_id
@@ -184,7 +184,7 @@ let check_decl_position env sign d =
   let needed = global_vars_set_of_decl env d in
   let deps = dependency_closure env (named_context_of_val sign) needed in
   if Id.List.mem x deps then
-    errorlabstrm "Logic.check_decl_position"
+    user_err ~hdr:"Logic.check_decl_position"
       (str "Cannot create self-referring hypothesis " ++ pr_id x);
   x::deps
 
@@ -254,7 +254,7 @@ let move_hyp toleft (left,declfrom,right) hto =
 	    if not (move_location_eq hto (MoveAfter hyp)) then
 	      (first, d::middle)
             else
-	      errorlabstrm "move_hyp" (str "Cannot move " ++ pr_id (NamedDecl.get_id declfrom) ++
+	      user_err ~hdr:"move_hyp" (str "Cannot move " ++ pr_id (NamedDecl.get_id declfrom) ++
 	        Miscprint.pr_move_location pr_id hto ++
 	        str (if toleft then ": it occurs in " else ": it depends on ")
 	        ++ pr_id hyp ++ str ".")
@@ -289,7 +289,7 @@ let move_hyp toleft (left,declfrom,right) hto =
 variables only in Application and Case *)
 
 let error_unsupported_deep_meta c =
-  errorlabstrm "" (strbrk "Application of lemmas whose beta-iota normal " ++
+  user_err  (strbrk "Application of lemmas whose beta-iota normal " ++
     strbrk "form contains metavariables deep inside the term is not " ++
     strbrk "supported; try \"refine\" instead.")
 
@@ -501,10 +501,10 @@ let convert_hyp check sign sigma d =
         let c = NamedDecl.get_value d' in
         let env = Global.env_of_context sign in
         if check && not (is_conv env sigma (NamedDecl.get_type d) (NamedDecl.get_type d')) then
-	  errorlabstrm "Logic.convert_hyp"
+	  user_err ~hdr:"Logic.convert_hyp"
             (str "Incorrect change of the type of " ++ pr_id id ++ str ".");
         if check && not (Option.equal (is_conv env sigma) b c) then
-	  errorlabstrm "Logic.convert_hyp"
+	  user_err ~hdr:"Logic.convert_hyp"
             (str "Incorrect change of the body of "++ pr_id id ++ str ".");
        if check then reorder := check_decl_position env sign d;
        d) in
@@ -537,7 +537,7 @@ let prim_refiner r sigma goal =
 	      t,cl,sigma
 	  else
             (if !check && mem_named_context id (named_context_of_val sign) then
-	      errorlabstrm "Logic.prim_refiner"
+	      user_err ~hdr:"Logic.prim_refiner"
                 (str "Variable " ++ pr_id id ++ str " is already declared.");
 	     push_named_context_val (LocalAssum (id,t)) sign,t,cl,sigma) in
         let (sg2,ev2,sigma) =