diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-07-05 01:49:27 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-07-05 01:49:27 +0000 |
| commit | a778b72e3ebfbe784fbe55ee5e124ba3f66cfb10 (patch) | |
| tree | 45ccc4afcf8edc5aed09d76b45c826a1e779af66 /lib/genarg.mli | |
| parent | 556c2ce6f1b09d09484cc83f6ada213496add45b (diff) | |
Expurgating the useless difference between List0 and List1 at the
level of generic arguments. This only matters at parsing time.
TODO: the current status is not satisfactory enough, as rule
emptyness is still decided w.r.t. generic arguments. This should be
done on a grammar entry basis instead.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16617 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/genarg.mli')
| -rw-r--r-- | lib/genarg.mli | 16 |
1 files changed, 4 insertions, 12 deletions
diff --git a/lib/genarg.mli b/lib/genarg.mli index 8152a19ed..a7232c6bd 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -162,10 +162,7 @@ val top_unpack : 'r top_unpack -> tlevel generic_argument -> 'r Those functions fail if they are applied to an argument which has not the right dynamic type. *) -val fold_list0 : - ('a generic_argument -> 'c -> 'c) -> 'a generic_argument -> 'c -> 'c - -val fold_list1 : +val fold_list : ('a generic_argument -> 'c -> 'c) -> 'a generic_argument -> 'c -> 'c val fold_opt : @@ -178,10 +175,7 @@ val fold_pair : (** [app_list0] fails if applied to an argument not of tag [List0 t] for some [t]; it's the responsability of the caller to ensure it *) -val app_list0 : ('a generic_argument -> 'b generic_argument) -> -'a generic_argument -> 'b generic_argument - -val app_list1 : ('a generic_argument -> 'b generic_argument) -> +val app_list : ('a generic_argument -> 'b generic_argument) -> 'a generic_argument -> 'b generic_argument val app_opt : ('a generic_argument -> 'b generic_argument) -> @@ -210,8 +204,7 @@ type argument_type = | ConstrWithBindingsArgType | BindingsArgType | RedExprArgType - | List0ArgType of argument_type - | List1ArgType of argument_type + | ListArgType of argument_type | OptArgType of argument_type | PairArgType of argument_type * argument_type | ExtraArgType of string @@ -250,8 +243,7 @@ end (** {6 Parameterized types} *) -val wit_list0 : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type -val wit_list1 : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type +val wit_list : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type val wit_opt : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type val wit_pair : ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type -> ('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type |