From cb2f6a95ee72edb956f419a24f8385c8ae7f96f4 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 28 Dec 2015 02:08:42 +0100 Subject: 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. --- lib/genarg.ml | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) (limited to 'lib/genarg.ml') 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 -- cgit v1.2.3