aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf/glob_term.mli
diff options
context:
space:
mode:
Diffstat (limited to 'intf/glob_term.mli')
-rw-r--r--intf/glob_term.mli6
1 files changed, 3 insertions, 3 deletions
diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index 5aa5bdeeb..aefccd518 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 Loc.located
+and cases_pattern = cases_pattern_r CAst.ast
(** 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 Loc.located
+and glob_constr = glob_constr_r CAst.ast
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 Loc.located
+and extended_glob_local_binder = extended_glob_local_binder_r CAst.ast
(** A globalised term together with a closure representing the value
of its free variables. Intended for use when these variables are taken