diff options
| -rw-r--r-- | interp/constrintern.ml | 2 | ||||
| -rw-r--r-- | intf/constrexpr.mli | 6 | ||||
| -rw-r--r-- | intf/glob_term.mli | 6 | ||||
| -rw-r--r-- | lib/cAst.ml | 2 | ||||
| -rw-r--r-- | lib/cAst.mli | 14 |
5 files changed, 15 insertions, 15 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 7dc364e5d..3b3dccc99 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -893,7 +893,7 @@ type raw_cases_pattern_expr_r = (** [RCPatCstr (loc, c, l1, l2)] represents ((@c l1) l2) *) | RCPatAtom of Id.t option | RCPatOr of raw_cases_pattern_expr list -and raw_cases_pattern_expr = raw_cases_pattern_expr_r CAst.ast +and raw_cases_pattern_expr = raw_cases_pattern_expr_r CAst.t (** {6 Elementary bricks } *) let apply_scope_env env = function diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index d54ad8bee..614c097b5 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -52,7 +52,7 @@ type cases_pattern_expr_r = | CPatRecord of (reference * cases_pattern_expr) list | CPatDelimiters of string * cases_pattern_expr | CPatCast of cases_pattern_expr * constr_expr -and cases_pattern_expr = cases_pattern_expr_r CAst.ast +and cases_pattern_expr = cases_pattern_expr_r CAst.t and cases_pattern_notation_substitution = cases_pattern_expr list * (** for constr subterms *) @@ -89,7 +89,7 @@ and constr_expr_r = | CGeneralization of binding_kind * abstraction_kind option * constr_expr | CPrim of prim_token | CDelimiters of string * constr_expr -and constr_expr = constr_expr_r CAst.ast +and constr_expr = constr_expr_r CAst.t and case_expr = constr_expr (* expression that is being matched *) * Name.t Loc.located option (* as-clause *) @@ -140,4 +140,4 @@ type module_ast_r = | CMident of qualid | CMapply of module_ast * module_ast | CMwith of module_ast * with_declaration_ast -and module_ast = module_ast_r CAst.ast +and module_ast = module_ast_r CAst.t diff --git a/intf/glob_term.mli b/intf/glob_term.mli index aefccd518..33c71884a 100644 --- a/intf/glob_term.mli +++ b/intf/glob_term.mli @@ -28,7 +28,7 @@ type cases_pattern_r = | PatVar of Name.t | PatCstr of constructor * cases_pattern list * Name.t (** [PatCstr(p,C,l,x)] = "|'C' 'l' as 'x'" *) -and cases_pattern = cases_pattern_r CAst.ast +and cases_pattern = cases_pattern_r CAst.t (** Representation of an internalized (or in other words globalized) term. *) type glob_constr_r = @@ -53,7 +53,7 @@ type glob_constr_r = | GSort of glob_sort | GHole of Evar_kinds.t * intro_pattern_naming_expr * Genarg.glob_generic_argument option | GCast of glob_constr * glob_constr cast_type -and glob_constr = glob_constr_r CAst.ast +and glob_constr = glob_constr_r CAst.t and glob_decl = Name.t * binding_kind * glob_constr option * glob_constr @@ -83,7 +83,7 @@ type extended_glob_local_binder_r = | GLocalAssum of Name.t * binding_kind * glob_constr | GLocalDef of Name.t * binding_kind * glob_constr * glob_constr option | GLocalPattern of (cases_pattern * Id.t list) * Id.t * binding_kind * glob_constr -and extended_glob_local_binder = extended_glob_local_binder_r CAst.ast +and extended_glob_local_binder = extended_glob_local_binder_r CAst.t (** A globalised term together with a closure representing the value of its free variables. Intended for use when these variables are taken diff --git a/lib/cAst.ml b/lib/cAst.ml index f0a405776..301a6bac8 100644 --- a/lib/cAst.ml +++ b/lib/cAst.ml @@ -7,7 +7,7 @@ (************************************************************************) (** The ast type contains generic metadata for AST nodes. *) -type 'a ast = { +type 'a t = { v : 'a; loc : Loc.t option; } diff --git a/lib/cAst.mli b/lib/cAst.mli index 291536d12..700a06ce8 100644 --- a/lib/cAst.mli +++ b/lib/cAst.mli @@ -7,16 +7,16 @@ (************************************************************************) (** The ast type contains generic metadata for AST nodes *) -type 'a ast = private { +type 'a t = private { v : 'a; loc : Loc.t option; } -val make : ?loc:Loc.t -> 'a -> 'a ast +val make : ?loc:Loc.t -> 'a -> 'a t -val map : ('a -> 'b) -> 'a ast -> 'b ast -val map_with_loc : (?loc:Loc.t -> 'a -> 'b) -> 'a ast -> 'b ast -val map_from_loc : (?loc:Loc.t -> 'a -> 'b) -> 'a Loc.located -> 'b ast +val map : ('a -> 'b) -> 'a t -> 'b t +val map_with_loc : (?loc:Loc.t -> 'a -> 'b) -> 'a t -> 'b t +val map_from_loc : (?loc:Loc.t -> 'a -> 'b) -> 'a Loc.located -> 'b t -val with_val : ('a -> 'b) -> 'a ast -> 'b -val with_loc_val : (?loc:Loc.t -> 'a -> 'b) -> 'a ast -> 'b +val with_val : ('a -> 'b) -> 'a t -> 'b +val with_loc_val : (?loc:Loc.t -> 'a -> 'b) -> 'a t -> 'b |