aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/genarg.ml
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-01-28 21:05:35 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-01-28 21:05:35 +0000
commit5a39e6c08d428d774165e0ef3922ba8b75eee9e1 (patch)
treee035f490e2c748356df73342876b22cfcb3bc5a0 /interp/genarg.ml
parent5e8824960f68f529869ac299b030282cc916ba2c (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 'interp/genarg.ml')
-rw-r--r--interp/genarg.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 382c38da3..a029a3b31 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Pp
open Util
open Glob_term
open Constrexpr
@@ -238,7 +239,7 @@ type ('a,'b) abstract_argument_type = argument_type
let create_arg v s =
if List.mem_assoc s !dyntab then
- Errors.anomaly ("Genarg.create: already declared generic argument " ^ s);
+ Errors.anomaly ~label:"Genarg.create" (str ("already declared generic argument " ^ s));
let t = ExtraArgType s in
dyntab := (s,Option.map (in_gen t) v) :: !dyntab;
(t,t,t)