diff options
| author | Pierre Letouzey | 2016-06-27 11:03:43 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-07-03 12:08:03 +0200 |
| commit | f14b6f1a17652566f0cbc00ce81421ba0684dad5 (patch) | |
| tree | 8a331593d0d1b518e8764c92ac54e3b11c222358 /plugins/decl_mode | |
| parent | 500d38d0887febb614ddcadebaef81e0c7942584 (diff) | |
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
Diffstat (limited to 'plugins/decl_mode')
| -rw-r--r-- | plugins/decl_mode/decl_interp.ml | 2 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_mode.ml | 2 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 6 | ||||
| -rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 2 | ||||
| -rw-r--r-- | plugins/decl_mode/ppdecl_proof.ml | 2 |
5 files changed, 7 insertions, 7 deletions
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index c0ef343059..10c09c8d6b 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Constrexpr diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml index f9399d6824..92d4089015 100644 --- a/plugins/decl_mode/decl_mode.ml +++ b/plugins/decl_mode/decl_mode.ml @@ -9,7 +9,7 @@ open Names open Term open Evd -open Errors +open CErrors open Util let daimon_flag = ref false diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index b6c34d2703..5ed426c1df 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Pp open Evd @@ -277,7 +277,7 @@ let prepare_goal items gls = filter_hyps (let keep = !tokeep in fun id -> Id.Set.mem id keep)] gls let my_automation_tac = ref - (Proofview.tclZERO (Errors.make_anomaly (Pp.str"No automation registered"))) + (Proofview.tclZERO (CErrors.make_anomaly (Pp.str"No automation registered"))) let register_automation_tac tac = my_automation_tac:= tac @@ -415,7 +415,7 @@ let find_subsubgoal c ctyp skip submetas gls = se.se_meta submetas se.se_meta_list} else dfs (pred n) - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> begin enstack_subsubgoals env se stack gls; dfs n diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 73d3d1bab8..6c17dcc4f1 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -58,7 +58,7 @@ let interp_proof_instr _ { Evd.it = gl ; sigma = sigma }= let vernac_decl_proof () = let pf = Proof_global.give_me_the_proof () in if Proof.is_done pf then - Errors.error "Nothing left to prove here." + CErrors.error "Nothing left to prove here." else begin Decl_proof_instr.go_to_proof_mode () ; diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml index 4c71f04107..59a0bb5a2d 100644 --- a/plugins/decl_mode/ppdecl_proof.ml +++ b/plugins/decl_mode/ppdecl_proof.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Pp open Decl_expr open Names |