aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--interp/constrintern.ml2
-rw-r--r--intf/constrexpr.mli6
-rw-r--r--intf/glob_term.mli6
-rw-r--r--lib/cAst.ml2
-rw-r--r--lib/cAst.mli14
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