diff options
Diffstat (limited to 'lib/genarg.ml')
| -rw-r--r-- | lib/genarg.ml | 33 |
1 files changed, 18 insertions, 15 deletions
diff --git a/lib/genarg.ml b/lib/genarg.ml index 05c828d5..209d1b27 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp @@ -11,7 +13,7 @@ open Util module ArgT = struct - module DYN = Dyn.Make(struct end) + module DYN = Dyn.Make () module Map = DYN.Map type ('a, 'b, 'c) tag = ('a * 'b * 'c) DYN.tag type any = Any : ('a, 'b, 'c) tag -> any @@ -58,7 +60,7 @@ fun t1 t2 -> match t1, t2 with end | _ -> None -let rec pr_genarg_type : type a b c. (a, b, c) genarg_type -> std_ppcmds = function +let rec pr_genarg_type : type a b c. (a, b, c) genarg_type -> Pp.t = function | ListArg t -> pr_genarg_type t ++ spc () ++ str "list" | OptArg t -> pr_genarg_type t ++ spc () ++ str "opt" | PairArg (t1, t2) -> @@ -159,7 +161,7 @@ let create_arg name = match ArgT.name name with | None -> ExtraArg (ArgT.create name) | Some _ -> - CErrors.anomaly (str "generic argument already declared: " ++ str name) + CErrors.anomaly (str "generic argument already declared: " ++ str name ++ str ".") let make0 = create_arg @@ -172,19 +174,22 @@ sig val default : ('raw, 'glb, 'top) genarg_type -> ('raw, 'glb, 'top) obj option end +let get_arg_tag = function +| ExtraArg s -> s +| _ -> assert false + module Register (M : GenObj) = struct module GenMap = ArgMap(struct type ('r, 'g, 't) t = ('r, 'g, 't) M.obj end) let arg0_map = ref GenMap.empty - let register0 arg f = match arg with - | ExtraArg s -> + let register0 arg f = + let s = get_arg_tag arg in if GenMap.mem s !arg0_map then - let msg = str M.name ++ str " function already registered: " ++ str (ArgT.repr s) in + let msg = str M.name ++ str " function already registered: " ++ str (ArgT.repr s) ++ str "." in CErrors.anomaly msg else arg0_map := GenMap.add s (GenMap.Pack f) !arg0_map - | _ -> assert false let get_obj0 name = try @@ -192,13 +197,11 @@ struct with Not_found -> match M.default (ExtraArg name) with | None -> - CErrors.anomaly (str M.name ++ str " function not found: " ++ str (ArgT.repr name)) + CErrors.anomaly (str M.name ++ str " function not found: " ++ str (ArgT.repr name) ++ str ".") | Some obj -> obj (** For now, the following function is quite dummy and should only be applied to an extra argument type, otherwise, it will badly fail. *) - let obj t = match t with - | ExtraArg s -> get_obj0 s - | _ -> assert false + let obj t = get_obj0 @@ get_arg_tag t end |