diff options
author | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
commit | 870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch) | |
tree | 0c647056de1832cf1dba5ba58758b9121418e4be /interp/genarg.mli | |
parent | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff) |
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
Diffstat (limited to 'interp/genarg.mli')
-rw-r--r-- | interp/genarg.mli | 21 |
1 files changed, 11 insertions, 10 deletions
diff --git a/interp/genarg.mli b/interp/genarg.mli index 3548585b..da175078 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 10753 2008-04-04 14:55:47Z herbelin $ i*) +(*i $Id: genarg.mli 11309 2008-08-06 10:30:35Z herbelin $ i*) open Util open Names @@ -32,16 +32,16 @@ type open_rawconstr = unit * rawconstr_and_expr type 'a with_ebindings = 'a * open_constr bindings type intro_pattern_expr = - | IntroOrAndPattern of case_intro_pattern_expr + | IntroOrAndPattern of or_and_intro_pattern_expr | IntroWildcard - | IntroIdentifier of identifier - | IntroAnonymous | IntroRewrite of bool + | IntroIdentifier of identifier | IntroFresh of identifier -and case_intro_pattern_expr = intro_pattern_expr list list + | IntroAnonymous +and or_and_intro_pattern_expr = (loc * intro_pattern_expr) list list -val pr_intro_pattern : intro_pattern_expr -> Pp.std_ppcmds -val pr_case_intro_pattern : case_intro_pattern_expr -> Pp.std_ppcmds +val pr_intro_pattern : intro_pattern_expr located -> Pp.std_ppcmds +val pr_or_and_intro_pattern : or_and_intro_pattern_expr -> Pp.std_ppcmds (* The route of a generic argument, from parsing to evaluation @@ -128,15 +128,16 @@ val wit_int_or_var : (int or_var,tlevel) abstract_argument_type val rawwit_string : (string,rlevel) abstract_argument_type val globwit_string : (string,glevel) abstract_argument_type + val wit_string : (string,tlevel) abstract_argument_type val rawwit_pre_ident : (string,rlevel) abstract_argument_type val globwit_pre_ident : (string,glevel) abstract_argument_type val wit_pre_ident : (string,tlevel) abstract_argument_type -val rawwit_intro_pattern : (intro_pattern_expr,rlevel) abstract_argument_type -val globwit_intro_pattern : (intro_pattern_expr,glevel) abstract_argument_type -val wit_intro_pattern : (intro_pattern_expr,tlevel) abstract_argument_type +val rawwit_intro_pattern : (intro_pattern_expr located,rlevel) abstract_argument_type +val globwit_intro_pattern : (intro_pattern_expr located,glevel) abstract_argument_type +val wit_intro_pattern : (intro_pattern_expr located,tlevel) abstract_argument_type val rawwit_ident : (identifier,rlevel) abstract_argument_type val globwit_ident : (identifier,glevel) abstract_argument_type |