diff options
Diffstat (limited to 'interp/genarg.ml')
| -rw-r--r-- | interp/genarg.ml | 26 |
1 files changed, 17 insertions, 9 deletions
diff --git a/interp/genarg.ml b/interp/genarg.ml index 77ed1fe6..49c157f2 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: genarg.ml 8926 2006-06-08 20:23:17Z herbelin $ *) +(* $Id: genarg.ml 10753 2008-04-04 14:55:47Z herbelin $ *) open Pp open Util @@ -16,6 +16,7 @@ open Nametab open Rawterm open Topconstr open Term +open Evd type argument_type = (* Basic types *) @@ -44,19 +45,25 @@ type argument_type = | ExtraArgType of string type 'a and_short_name = 'a * identifier located option +type 'a or_by_notation = AN of 'a | ByNotation of loc * string + type rawconstr_and_expr = rawconstr * constr_expr option +type open_constr_expr = unit * constr_expr +type open_rawconstr = unit * rawconstr_and_expr + +type 'a with_ebindings = 'a * open_constr bindings (* Dynamics but tagged by a type expression *) -type ('a,'b) generic_argument = argument_type * Obj.t +type 'a generic_argument = argument_type * Obj.t let dyntab = ref ([] : string list) type rlevel = constr_expr type glevel = rawconstr_and_expr -type tlevel = constr +type tlevel = open_constr -type ('a,'b,'c) abstract_argument_type = argument_type +type ('a,'b) abstract_argument_type = argument_type let create_arg s = if List.mem s !dyntab then @@ -72,6 +79,8 @@ type intro_pattern_expr = | IntroWildcard | IntroIdentifier of identifier | IntroAnonymous + | IntroRewrite of bool + | IntroFresh of identifier and case_intro_pattern_expr = intro_pattern_expr list list let rec pr_intro_pattern = function @@ -79,6 +88,9 @@ let rec pr_intro_pattern = function | IntroWildcard -> str "_" | IntroIdentifier id -> pr_id id | IntroAnonymous -> str "?" + | IntroRewrite true -> str "->" + | IntroRewrite false -> str "<-" + | IntroFresh id -> str "?" ++ pr_id id and pr_case_intro_pattern = function | [pl] -> @@ -88,10 +100,6 @@ and pr_case_intro_pattern = function hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll) ++ str "]" -type open_constr = Evd.evar_map * Term.constr -type open_constr_expr = unit * constr_expr -type open_rawconstr = unit * rawconstr_and_expr - let rawwit_bool = BoolArgType let globwit_bool = BoolArgType let wit_bool = BoolArgType @@ -218,7 +226,7 @@ let app_list1 f = function let app_opt f = function | (OptArgType t as u, l) -> let o = Obj.magic l in - (u, Obj.repr (option_map (fun x -> out_gen t (f (in_gen t x))) o)) + (u, Obj.repr (Option.map (fun x -> out_gen t (f (in_gen t x))) o)) | _ -> failwith "Genarg: not an opt" let app_pair f1 f2 = function |