diff options
Diffstat (limited to 'interp/genarg.ml')
| -rw-r--r-- | interp/genarg.ml | 23 |
1 files changed, 16 insertions, 7 deletions
diff --git a/interp/genarg.ml b/interp/genarg.ml index 1da428be..c9ba20e6 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: genarg.ml 11481 2008-10-20 19:23:51Z herbelin $ *) +(* $Id$ *) open Pp open Util @@ -47,12 +47,18 @@ type argument_type = type 'a and_short_name = 'a * identifier located option type 'a or_by_notation = | AN of 'a - | ByNotation of loc * string * Notation.delimiters option + | ByNotation of (loc * string * Notation.delimiters option) + +let loc_of_or_by_notation f = function + | AN c -> f c + | ByNotation (loc,s,_) -> loc type rawconstr_and_expr = rawconstr * constr_expr option type open_constr_expr = unit * constr_expr type open_rawconstr = unit * rawconstr_and_expr +type rawconstr_pattern_and_expr = rawconstr_and_expr * Pattern.constr_pattern + type 'a with_ebindings = 'a * open_constr bindings (* Dynamics but tagged by a type expression *) @@ -61,9 +67,9 @@ type 'a generic_argument = argument_type * Obj.t let dyntab = ref ([] : string list) -type rlevel = constr_expr -type glevel = rawconstr_and_expr -type tlevel = open_constr +type rlevel +type glevel +type tlevel type ('a,'b) abstract_argument_type = argument_type @@ -82,6 +88,7 @@ type intro_pattern_expr = | IntroRewrite of bool | IntroIdentifier of identifier | IntroFresh of identifier + | IntroForthcoming of bool | IntroAnonymous and or_and_intro_pattern_expr = (loc * intro_pattern_expr) list list @@ -92,11 +99,13 @@ let rec pr_intro_pattern (_,pat) = match pat with | IntroRewrite false -> str "<-" | IntroIdentifier id -> pr_id id | IntroFresh id -> str "?" ++ pr_id id + | IntroForthcoming true -> str "*" + | IntroForthcoming false -> str "**" | IntroAnonymous -> str "?" and pr_or_and_intro_pattern = function | [pl] -> - str "(" ++ hv 0 (prlist_with_sep pr_coma pr_intro_pattern pl) ++ str ")" + str "(" ++ hv 0 (prlist_with_sep pr_comma pr_intro_pattern pl) ++ str ")" | pll -> str "[" ++ hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll) @@ -163,7 +172,7 @@ let globwit_constr_may_eval = ConstrMayEvalArgType let wit_constr_may_eval = ConstrMayEvalArgType let rawwit_open_constr_gen b = OpenConstrArgType b -let globwit_open_constr_gen b = OpenConstrArgType b +let globwit_open_constr_gen b = OpenConstrArgType b let wit_open_constr_gen b = OpenConstrArgType b let rawwit_open_constr = rawwit_open_constr_gen false |