diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/genarg.ml | 16 | ||||
| -rw-r--r-- | interp/genarg.mli | 13 |
2 files changed, 23 insertions, 6 deletions
diff --git a/interp/genarg.ml b/interp/genarg.ml index d1eda47b78..35107c8080 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -26,7 +26,7 @@ type argument_type = | StringArgType | PreIdentArgType | IntroPatternArgType - | IdentArgType + | IdentArgType of bool | VarArgType | RefArgType (* Specific types *) @@ -126,9 +126,17 @@ let rawwit_intro_pattern = IntroPatternArgType let globwit_intro_pattern = IntroPatternArgType let wit_intro_pattern = IntroPatternArgType -let rawwit_ident = IdentArgType -let globwit_ident = IdentArgType -let wit_ident = IdentArgType +let rawwit_ident_gen b = IdentArgType b +let globwit_ident_gen b = IdentArgType b +let wit_ident_gen b = IdentArgType b + +let rawwit_ident = rawwit_ident_gen true +let globwit_ident = globwit_ident_gen true +let wit_ident = wit_ident_gen true + +let rawwit_pattern_ident = rawwit_ident_gen false +let globwit_pattern_ident = globwit_ident_gen false +let wit_pattern_ident = wit_ident_gen false let rawwit_var = VarArgType let globwit_var = VarArgType diff --git a/interp/genarg.mli b/interp/genarg.mli index 0ced1e5bea..92c7db36f4 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -86,7 +86,8 @@ IntArgType int int IntOrVarArgType int or_var int StringArgType string (parsed w/ "") string PreIdentArgType string (parsed w/o "") (vernac only) -IdentArgType identifier identifier +IdentArgType true identifier identifier +IdentArgType false identifier (pattern_ident) identifier IntroPatternArgType intro_pattern_expr intro_pattern_expr VarArgType identifier located identifier RefArgType reference global_reference @@ -145,6 +146,14 @@ val rawwit_ident : (identifier,rlevel) abstract_argument_type val globwit_ident : (identifier,glevel) abstract_argument_type val wit_ident : (identifier,tlevel) abstract_argument_type +val rawwit_pattern_ident : (identifier,rlevel) abstract_argument_type +val globwit_pattern_ident : (identifier,glevel) abstract_argument_type +val wit_pattern_ident : (identifier,tlevel) abstract_argument_type + +val rawwit_ident_gen : bool -> (identifier,rlevel) abstract_argument_type +val globwit_ident_gen : bool -> (identifier,glevel) abstract_argument_type +val wit_ident_gen : bool -> (identifier,tlevel) abstract_argument_type + val rawwit_var : (identifier located,rlevel) abstract_argument_type val globwit_var : (identifier located,glevel) abstract_argument_type val wit_var : (identifier,tlevel) abstract_argument_type @@ -257,7 +266,7 @@ type argument_type = | StringArgType | PreIdentArgType | IntroPatternArgType - | IdentArgType + | IdentArgType of bool | VarArgType | RefArgType (* Specific types *) |