aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-04-09 03:35:20 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-04-25 00:33:36 +0200
commitee2197096fe75a63b4d92cb3a1bb05122c5c625b (patch)
tree3b40c06375a463625a2675b90e009fcb0b64a7d2 /intf
parent054d2736c1c1b55cb7708ff0444af521cd0fe2ba (diff)
[location] [ast] Port module AST to CAst
Diffstat (limited to 'intf')
-rw-r--r--intf/constrexpr.mli2
-rw-r--r--intf/glob_term.mli6
2 files changed, 4 insertions, 4 deletions
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index 4f1e9d8e6..5366a302e 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -149,4 +149,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 Loc.located
+and module_ast = module_ast_r CAst.ast
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