aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--interp/constrarg.ml3
-rw-r--r--lib/genarg.ml3
-rw-r--r--lib/genarg.mli3
-rw-r--r--parsing/pcoq.ml22
-rw-r--r--printing/pptactic.ml11
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