diff options
Diffstat (limited to 'interp/genarg.mli')
| -rw-r--r-- | interp/genarg.mli | 19 |
1 files changed, 15 insertions, 4 deletions
diff --git a/interp/genarg.mli b/interp/genarg.mli index da175078..86b19de7 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: genarg.mli 11309 2008-08-06 10:30:35Z herbelin $ i*) +(*i $Id: genarg.mli 11481 2008-10-20 19:23:51Z herbelin $ i*) open Util open Names @@ -19,7 +19,9 @@ open Evd type 'a and_short_name = 'a * identifier located option -type 'a or_by_notation = AN of 'a | ByNotation of loc * string +type 'a or_by_notation = + | AN of 'a + | ByNotation of loc * string * Notation.delimiters option (* In globalize tactics, we need to keep the initial [constr_expr] to recompute*) (* in the environment by the effective calls to Intro, Inversion, etc *) @@ -84,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 @@ -143,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 @@ -255,7 +266,7 @@ type argument_type = | StringArgType | PreIdentArgType | IntroPatternArgType - | IdentArgType + | IdentArgType of bool | VarArgType | RefArgType (* Specific types *) |