diff options
author | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
commit | cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch) | |
tree | b7832bd5d412a5a5d69cb36ae2ded62c71124c22 /interp/genarg.mli | |
parent | 113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff) |
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
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 *) |