diff options
| author |  Matej Košík <matej.kosik@inria.fr> | 2017-04-28 14:31:14 +0200 |
|---|---|---|
| committer |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-05-24 17:41:35 +0200 |
| commit | 209956322367e5a4a4c8c78c053ea9352a9a16c8 (patch) | |
| tree | cba5cbe9d65d51a2c351bea8c1b2f9714d561d71 /intf | |
| parent | 6f2c19a1054ce58927dfa5b33131c3665fd5fdf8 (diff) | |
[location] Renaming "CAst.ast" to "CAst.t"
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/constrexpr.mli | 6 | ||||
| -rw-r--r-- | intf/glob_term.mli | 6 |
2 files changed, 6 insertions, 6 deletions
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 |