diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-28 02:08:42 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-28 02:18:25 +0100 |
| commit | cb2f6a95ee72edb956f419a24f8385c8ae7f96f4 (patch) | |
| tree | 2ddf7103c75e4e824d5bfefade3ec774498fc131 /lib/genarg.ml | |
| parent | 28d4740736e5ef3b6f8547710dcf7e5b4d11cabd (diff) | |
Removing the special status of open_constr generic argument.
We also intepret it at toplevel as a true constr and push the resulting
evarmap in the current state.
Diffstat (limited to 'lib/genarg.ml')
| -rw-r--r-- | lib/genarg.ml | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/lib/genarg.ml b/lib/genarg.ml index 2b8e0c9fd..6108c1555 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -61,7 +61,6 @@ type argument_type = | VarArgType (* Specific types *) | ConstrArgType - | OpenConstrArgType | ListArgType of argument_type | OptArgType of argument_type | PairArgType of argument_type * argument_type @@ -71,7 +70,6 @@ let rec argument_type_eq arg1 arg2 = match arg1, arg2 with | IdentArgType, IdentArgType -> true | VarArgType, VarArgType -> true | ConstrArgType, ConstrArgType -> true -| OpenConstrArgType, OpenConstrArgType -> true | ListArgType arg1, ListArgType arg2 -> argument_type_eq arg1 arg2 | OptArgType arg1, OptArgType arg2 -> argument_type_eq arg1 arg2 | PairArgType (arg1l, arg1r), PairArgType (arg2l, arg2r) -> @@ -83,7 +81,6 @@ let rec pr_argument_type = function | IdentArgType -> str "ident" | VarArgType -> str "var" | ConstrArgType -> str "constr" -| OpenConstrArgType -> str "open_constr" | ListArgType t -> pr_argument_type t ++ spc () ++ str "list" | OptArgType t -> pr_argument_type t ++ spc () ++ str "opt" | PairArgType (t1, t2) -> @@ -210,14 +207,12 @@ let base_create n = Val.Base (Dyn.create n) let ident_T = base_create "ident" let genarg_T = base_create "genarg" let constr_T = base_create "constr" -let open_constr_T = base_create "open_constr" let rec val_tag = function | IdentArgType -> cast_tag ident_T | VarArgType -> cast_tag ident_T (** Must ensure that toplevel types of Var and Ident agree! *) | ConstrArgType -> cast_tag constr_T -| OpenConstrArgType -> cast_tag open_constr_T | ExtraArgType s -> cast_tag (String.Map.find s !arg0_map).dyn | ListArgType t -> cast_tag (Val.List (val_tag t)) | OptArgType t -> cast_tag (Val.Opt (val_tag t)) @@ -240,7 +235,7 @@ fun wit v -> match unquote wit with | IdentArgType | VarArgType | ConstrArgType -| OpenConstrArgType | ExtraArgType _ -> try_prj wit v +| ExtraArgType _ -> try_prj wit v | ListArgType t -> let Val.Dyn (tag, v) = v in begin match tag with |