diff options
| -rw-r--r-- | interp/constrarg.ml | 3 | ||||
| -rw-r--r-- | lib/genarg.ml | 3 | ||||
| -rw-r--r-- | lib/genarg.mli | 3 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 22 | ||||
| -rw-r--r-- | printing/pptactic.ml | 11 |
5 files changed, 18 insertions, 24 deletions
diff --git a/interp/constrarg.ml b/interp/constrarg.ml index a8dfd02e1..f8957a24b 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -19,9 +19,6 @@ let loc_of_or_by_notation f = function | AN c -> f c | ByNotation (loc,s,_) -> loc -let unsafe_of_type (t : argument_type) : ('a, 'b, 'c) Genarg.genarg_type = - Obj.magic t - let wit_int_or_var = Genarg.make0 ~dyn:(val_tag (topwit Stdarg.wit_int)) None "int_or_var" diff --git a/lib/genarg.ml b/lib/genarg.ml index c2c1014f1..5efb07444 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -117,6 +117,9 @@ type 'a raw_abstract_argument_type = ('a,rlevel) abstract_argument_type type 'a glob_abstract_argument_type = ('a,glevel) abstract_argument_type type 'a typed_abstract_argument_type = ('a,tlevel) abstract_argument_type +let arg_list wit = ListArgType wit +let arg_opt wit = OptArgType wit + type ('a, 'b, 'c, 'l) cast = Obj.t let raw = Obj.obj diff --git a/lib/genarg.mli b/lib/genarg.mli index 56c09f14f..8099c062a 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -265,6 +265,9 @@ val wit_opt : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) gena val wit_pair : ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type -> ('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type +val arg_list : ('a, 'l) abstract_argument_type -> ('a list, 'l) abstract_argument_type +val arg_opt : ('a, 'l) abstract_argument_type -> ('a option, 'l) abstract_argument_type + (** {5 Magic used by the parser} *) val default_empty_value : ('raw, 'glb, 'top) genarg_type -> 'raw option diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 291e919d8..d5acf59f6 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -759,21 +759,11 @@ let atactic n = if n = 5 then Aentry (name_of_entry Tactic.binder_tactic) else Aentryl (name_of_entry Tactic.tactic_expr, n) -let unsafe_of_genarg : argument_type -> 'a raw_abstract_argument_type = - (** FIXME *) - Obj.magic - let try_get_entry u s = (** Order the effects: get_entry can raise Not_found *) let TypedEntry (typ, _) = get_entry u s in EntryName (typ, Aentry (Entry.unsafe_of_name (Entry.univ_name u, s))) -let wit_list : 'a raw_abstract_argument_type -> 'a list raw_abstract_argument_type = - fun t -> unsafe_of_genarg (ListArgType (unquote t)) - -let wit_opt : 'a raw_abstract_argument_type -> 'a option raw_abstract_argument_type = - fun t -> unsafe_of_genarg (OptArgType (unquote t)) - type _ target = | TgAny : 's target | TgTactic : int -> Tacexpr.raw_tactic_expr target @@ -823,22 +813,22 @@ let rec interp_entry_name up_level s sep = let rec eval = function | Ulist1 e -> let EntryName (t, g) = eval e in - EntryName (wit_list t, Alist1 g) + EntryName (arg_list t, Alist1 g) | Ulist1sep (e, sep) -> let EntryName (t, g) = eval e in - EntryName (wit_list t, Alist1sep (g, sep)) + EntryName (arg_list t, Alist1sep (g, sep)) | Ulist0 e -> let EntryName (t, g) = eval e in - EntryName (wit_list t, Alist0 g) + EntryName (arg_list t, Alist0 g) | Ulist0sep (e, sep) -> let EntryName (t, g) = eval e in - EntryName (wit_list t, Alist0sep (g, sep)) + EntryName (arg_list t, Alist0sep (g, sep)) | Uopt e -> let EntryName (t, g) = eval e in - EntryName (wit_opt t, Aopt g) + EntryName (arg_opt t, Aopt g) | Umodifiers e -> let EntryName (t, g) = eval e in - EntryName (wit_list t, Amodifiers g) + EntryName (arg_list t, Amodifiers g) | Uentry s -> begin try try_get_entry uprim s with Not_found -> diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 5bc242b2b..e7443fd02 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1354,11 +1354,12 @@ module Make let check_val_type t arg = let AnyArg t = t in - let t = Genarg.val_tag (Obj.magic t) in (** FIXME *) - let Val.Dyn (t', _) = arg in - match Genarg.Val.eq t t' with - | None -> false - | Some _ -> true +(* let t = Genarg.val_tag (Obj.magic t) in *) +(* let Val.Dyn (t', _) = arg in *) +(* match Genarg.Val.eq t t' with *) +(* | None -> false *) +(* | Some _ -> true *) + true (** FIXME *) let pr_alias pr lev key args = pr_alias_gen check_val_type pr lev key args |