diff options
Diffstat (limited to 'intf/glob_term.mli')
| -rw-r--r-- | intf/glob_term.mli | 6 |
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 |