diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-01-28 21:05:35 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-01-28 21:05:35 +0000 |
| commit | 5a39e6c08d428d774165e0ef3922ba8b75eee9e1 (patch) | |
| tree | e035f490e2c748356df73342876b22cfcb3bc5a0 /kernel/environ.ml | |
| parent | 5e8824960f68f529869ac299b030282cc916ba2c (diff) | |
Uniformization of the "anomaly" command.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 27b7c76b4..a36e2dcf6 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -460,13 +460,13 @@ fun env field value -> match value with | Const kn -> retroknowledge add_int31_op env value 2 op kn - | _ -> anomaly "Environ.register: should be a constant" + | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant") in let add_int31_unop_from_const op = match value with | Const kn -> retroknowledge add_int31_op env value 1 op kn - | _ -> anomaly "Environ.register: should be a constant" + | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant") in (* subfunction which completes the function constr_of_int31 above by performing the actual retroknowledge operations *) @@ -481,9 +481,9 @@ fun env field value -> | Ind i31t -> Retroknowledge.add_vm_decompile_constant_info rk value (constr_of_int31 i31t i31bit_type) - | _ -> anomaly "Environ.register: should be an inductive type") - | _ -> anomaly "Environ.register: Int31Bits should be an inductive type") - | _ -> anomaly "Environ.register: add_int31_decompilation_from_type called with an abnormal field" + | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type")) + | _ -> anomaly ~label:"Environ.register" (Pp.str "Int31Bits should be an inductive type")) + | _ -> anomaly ~label:"Environ.register" (Pp.str "add_int31_decompilation_from_type called with an abnormal field") in {env with retroknowledge = let retroknowledge_with_reactive_info = @@ -491,7 +491,7 @@ fun env field value -> | KInt31 (_, Int31Type) -> let i31c = match value with | Ind i31t -> (Construct (i31t, 1)) - | _ -> anomaly "Environ.register: should be an inductive type" + | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type") in add_int31_decompilation_from_type (add_vm_before_match_info @@ -511,14 +511,14 @@ fun env field value -> | Const kn -> retroknowledge add_int31_op env value 3 Cbytecodes.Kdiv21int31 kn - | _ -> anomaly "Environ.register: should be a constant") + | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant")) | KInt31 (_, Int31Div) -> add_int31_binop_from_const Cbytecodes.Kdivint31 | KInt31 (_, Int31AddMulDiv) -> (* this is a ternary operation *) (match value with | Const kn -> retroknowledge add_int31_op env value 3 Cbytecodes.Kaddmuldivint31 kn - | _ -> anomaly "Environ.register: should be a constant") + | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant")) | KInt31 (_, Int31Compare) -> add_int31_binop_from_const Cbytecodes.Kcompareint31 | KInt31 (_, Int31Head0) -> add_int31_unop_from_const Cbytecodes.Khead0int31 | KInt31 (_, Int31Tail0) -> add_int31_unop_from_const Cbytecodes.Ktail0int31 |