Merge branch 'cerrors-cclosure' into trunk

Was PR#226: CErrors & CClosure

10 files changed, 34 insertions, 33 deletions

diff --git a/ltac/evar_tactics.ml b/ltac/evar_tactics.ml
index 2e0996bf5a..30aeba3bbc 100644
--- a/ltac/evar_tactics.ml
+++ b/ltac/evar_tactics.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Util
-open Errors
+open CErrors
 open Evar_refiner
 open Tacmach
 open Tacexpr
diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4
index 8185a14d99..c6d72e03e2 100644
--- a/ltac/extraargs.ml4
+++ b/ltac/extraargs.ml4
@@ -90,7 +90,7 @@ let occurrences_of = function
   | n::_ as nl when n < 0 -> AllOccurrencesBut (List.map abs nl)
   | nl ->
       if List.exists (fun n -> n < 0) nl then
-        Errors.error "Illegal negative occurrence number.";
+        CErrors.error "Illegal negative occurrence number.";
       OnlyOccurrences nl
 
 let coerce_to_int v = match Value.to_int v with
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 725f2a5342..2ee9a6c982 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -19,7 +19,7 @@ open Mod_subst
 open Names
 open Tacexpr
 open Glob_ops
-open Errors
+open CErrors
 open Util
 open Evd
 open Termops
@@ -622,7 +622,7 @@ let hResolve id c occ t =
       Pretyping.understand env sigma t_hole
     with
       | Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _) as e ->
-          let (e, info) = Errors.push e in
+          let (e, info) = CErrors.push e in
           let loc = match Loc.get_loc info with None -> Loc.ghost | Some loc -> loc in
           resolve_hole (subst_hole_with_term (fst (Loc.unloc loc)) c_raw t_hole)
   in
@@ -641,7 +641,7 @@ let hResolve_auto id c t =
       hResolve id c n t
     with
     | UserError _ as e -> raise e
-    | e when Errors.noncritical e -> resolve_auto (n+1)
+    | e when CErrors.noncritical e -> resolve_auto (n+1)
   in
   resolve_auto 1
 
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index b5494a7cbb..9f2c0a93e7 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -36,7 +36,7 @@ let genarg_of_uconstr c = in_gen (rawwit Constrarg.wit_uconstr) c
 let reference_to_id = function
   | Libnames.Ident (loc, id) -> (loc, id)
   | Libnames.Qualid (loc,_) ->
-      Errors.user_err_loc (loc, "",
+      CErrors.user_err_loc (loc, "",
         str "This expression should be a simple identifier.")
 
 let tactic_mode = Gram.entry_create "vernac:tactic_command"
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 0b01eeef4d..0556191be8 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -8,7 +8,7 @@
 
 open Names
 open Pp
-open Errors
+open CErrors
 open Util
 open Nameops
 open Namegen
@@ -365,7 +365,7 @@ end) = struct
 	       rewrite_relation_class [| evar; mkApp (c, params) |] in
 	   let _ = Typeclasses.resolve_one_typeclass env' (goalevars evars) inst in
 	     Some (it_mkProd_or_LetIn t rels)
-	   with e when Errors.noncritical e -> None)
+	   with e when CErrors.noncritical e -> None)
   | _ -> None
 
 
@@ -446,7 +446,7 @@ let evd_convertible env evd x y =
     let evd = Evarconv.consider_remaining_unif_problems env evd in
     let () = Evarconv.check_problems_are_solved env evd in
     Some evd
-  with e when Errors.noncritical e -> None
+  with e when CErrors.noncritical e -> None
 
 let convertible env evd x y =
   Reductionops.is_conv_leq env evd x y
@@ -1407,7 +1407,7 @@ module Strategies =
 	let sigma, c = Pretyping.understand_tcc env (goalevars evars) c in
 	let unfolded =
 	  try Tacred.try_red_product env sigma c
-	  with e when Errors.noncritical e ->
+	  with e when CErrors.noncritical e ->
             error "fold: the term is not unfoldable !"
 	in
 	  try
@@ -1416,7 +1416,7 @@ module Strategies =
 	      state, Success { rew_car = ty; rew_from = t; rew_to = c';
 				  rew_prf = RewCast DEFAULTcast;
 				  rew_evars = (sigma, snd evars) }
-	  with e when Errors.noncritical e -> state, Fail
+	  with e when CErrors.noncritical e -> state, Fail
 					 }
   
 
@@ -1466,7 +1466,7 @@ let solve_constraints env (evars,cstrs) =
       (Typeclasses.mark_resolvables ~filter evars)
       
 let nf_zeta =
-  Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
+  Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
 
 exception RewriteFailure of Pp.std_ppcmds
 
@@ -1631,7 +1631,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
 
 let tactic_init_setoid () = 
   try init_setoid (); tclIDTAC
-  with e when Errors.noncritical e -> tclFAIL 0 (str"Setoid library not loaded")
+  with e when CErrors.noncritical e -> tclFAIL 0 (str"Setoid library not loaded")
 
 let cl_rewrite_clause_strat progress strat clause =
   tclTHEN (tactic_init_setoid ())
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index 6b7ae21f3c..673ac832a3 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Libobject
@@ -429,7 +429,7 @@ let register_ltac local tacl =
         let kn = Lib.make_kn id in
         let id_pp = pr_id id in
         let () = if is_defined_tac kn then
-          Errors.user_err_loc (loc, "",
+          CErrors.user_err_loc (loc, "",
             str "There is already an Ltac named " ++ id_pp ++ str".")
         in
         let is_shadowed =
@@ -437,7 +437,7 @@ let register_ltac local tacl =
             match Pcoq.parse_string Pcoq.Tactic.tactic (Id.to_string id) with
             | Tacexpr.TacArg _ -> false
             | _ -> true (* most probably TacAtom, i.e. a primitive tactic ident *)
-          with e when Errors.noncritical e -> true (* prim tactics with args, e.g. "apply" *)
+          with e when CErrors.noncritical e -> true (* prim tactics with args, e.g. "apply" *)
         in
         let () = if is_shadowed then warn_unusable_identifier id in
         NewTac id, body
@@ -446,7 +446,7 @@ let register_ltac local tacl =
         let kn =
           try Nametab.locate_tactic (snd (qualid_of_reference ident))
           with Not_found ->
-            Errors.user_err_loc (loc, "",
+            CErrors.user_err_loc (loc, "",
                         str "There is no Ltac named " ++ pr_reference ident ++ str ".")
         in
         UpdateTac kn, body
diff --git a/ltac/tacenv.ml b/ltac/tacenv.ml
index e3d5e18c9d..c709ab114e 100644
--- a/ltac/tacenv.ml
+++ b/ltac/tacenv.ml
@@ -24,7 +24,7 @@ let register_alias key tac =
 
 let interp_alias key =
   try KNmap.find key !alias_map
-  with Not_found -> Errors.anomaly (str "Unknown tactic alias: " ++ KerName.print key)
+  with Not_found -> CErrors.anomaly (str "Unknown tactic alias: " ++ KerName.print key)
 
 let check_alias key = KNmap.mem key !alias_map
 
@@ -55,7 +55,7 @@ let register_ml_tactic ?(overwrite = false) s (t : ml_tactic array) =
       if overwrite then
         tac_tab := MLTacMap.remove s !tac_tab
       else
-        Errors.anomaly (str "Cannot redeclare tactic " ++ pr_tacname s ++ str ".")
+        CErrors.anomaly (str "Cannot redeclare tactic " ++ pr_tacname s ++ str ".")
   in
   tac_tab := MLTacMap.add s t !tac_tab
 
@@ -65,7 +65,7 @@ let interp_ml_tactic { mltac_name = s; mltac_index = i } =
     let () = if Array.length tacs <= i then raise Not_found in
     tacs.(i)
   with Not_found ->
-    Errors.errorlabstrm ""
+    CErrors.errorlabstrm ""
       (str "The tactic " ++ pr_tacname s ++ str " is not installed.")
 
 (***************************************************************************)
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml
index 2bbb3b309b..00722ac285 100644
--- a/ltac/tacintern.ml
+++ b/ltac/tacintern.ml
@@ -11,7 +11,7 @@ open Pp
 open Genredexpr
 open Glob_term
 open Tacred
-open Errors
+open CErrors
 open Util
 open Names
 open Nameops
@@ -378,13 +378,13 @@ let dump_glob_red_expr = function
     try
       Dumpglob.add_glob (loc_of_or_by_notation Libnames.loc_of_reference r)
 	(Smartlocate.smart_global r)
-    with e when Errors.noncritical e -> ()) occs
+    with e when CErrors.noncritical e -> ()) occs
   | Cbv grf | Lazy grf ->
     List.iter (fun r ->
       try
         Dumpglob.add_glob (loc_of_or_by_notation Libnames.loc_of_reference r)
 	  (Smartlocate.smart_global r)
-      with e when Errors.noncritical e -> ()) grf.rConst
+      with e when CErrors.noncritical e -> ()) grf.rConst
   | _ -> ()
 
 let intern_red_expr ist = function
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 9a4beed871..397cd988da 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -13,7 +13,7 @@ open Genredexpr
 open Glob_term
 open Glob_ops
 open Tacred
-open Errors
+open CErrors
 open Util
 open Names
 open Nameops
@@ -209,7 +209,7 @@ let catching_error call_trace fail (e, info) =
   in
   if List.is_empty call_trace && List.is_empty inner_trace then fail (e, info)
   else begin
-    assert (Errors.noncritical e); (* preserved invariant *)
+    assert (CErrors.noncritical e); (* preserved invariant *)
     let new_trace = inner_trace @ call_trace in
     let located_exc = (e, Exninfo.add info ltac_trace_info new_trace) in
     fail located_exc
@@ -217,8 +217,8 @@ let catching_error call_trace fail (e, info) =
 
 let catch_error call_trace f x =
   try f x
-  with e when Errors.noncritical e ->
-    let e = Errors.push e in
+  with e when CErrors.noncritical e ->
+    let e = CErrors.push e in
     catching_error call_trace iraise e
 
 let catch_error_tac call_trace tac =
@@ -813,7 +813,7 @@ let interp_may_eval f ist env sigma = function
      try
 	f ist env sigma c
      with reraise ->
-       let reraise = Errors.push reraise in
+       let reraise = CErrors.push reraise in
        (* spiwack: to avoid unnecessary modifications of tacinterp, as this
           function already use effect, I call [run] hoping it doesn't mess
           up with any assumption. *)
@@ -827,7 +827,7 @@ let interp_constr_may_eval ist env sigma c =
     try
       interp_may_eval interp_constr ist env sigma c
     with reraise ->
-      let reraise = Errors.push reraise in
+      let reraise = CErrors.push reraise in
       (* spiwack: to avoid unnecessary modifications of tacinterp, as this
           function already use effect, I call [run] hoping it doesn't mess
           up with any assumption. *)
@@ -1867,7 +1867,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let env = Proofview.Goal.env gl in
         let sigma = project gl in
         let op = interp_typed_pattern ist env sigma op in
-        let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in
+        let to_catch = function Not_found -> true | e -> CErrors.is_anomaly e in
         let c_interp patvars = { Sigma.run = begin fun sigma ->
           let lfun' = Id.Map.fold (fun id c lfun ->
             Id.Map.add id (Value.of_constr c) lfun) 
diff --git a/ltac/tactic_debug.ml b/ltac/tactic_debug.ml
index 73d04b810d..e1c9fed637 100644
--- a/ltac/tactic_debug.ml
+++ b/ltac/tactic_debug.ml
@@ -36,10 +36,11 @@ type debug_info =
 
 (* An exception handler *)
 let explain_logic_error e =
-  Errors.print (fst (Cerrors.process_vernac_interp_error (e, Exninfo.null)))
+  CErrors.print (fst (ExplainErr.process_vernac_interp_error (e, Exninfo.null)))
 
 let explain_logic_error_no_anomaly e =
-  Errors.print_no_report (fst (Cerrors.process_vernac_interp_error (e, Exninfo.null)))
+  CErrors.print_no_report
+    (fst (ExplainErr.process_vernac_interp_error (e, Exninfo.null)))
 
 let msg_tac_debug s = Proofview.NonLogical.print_debug (s++fnl())
 let msg_tac_notice s = Proofview.NonLogical.print_notice (s++fnl())
@@ -417,4 +418,4 @@ let get_ltac_trace (_, info) =
   | None -> None
   | Some trace -> Some (extract_ltac_trace trace loc)
 
-let () = Cerrors.register_additional_error_info get_ltac_trace
+let () = ExplainErr.register_additional_error_info get_ltac_trace