diff options
| author | Maxime Dénès | 2016-09-20 17:13:27 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-09-20 17:18:37 +0200 |
| commit | 1bc1cba7a759a285131a3ed6ea8979716700b856 (patch) | |
| tree | 25202d41487d954621fb4bc42affd75bbae662cb /intf | |
| parent | aa29c92dfa395e2f369e81bd72cef482cdf90c65 (diff) | |
Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.
The new name makes it more obvious what is meant here by "kind". We leave
Decl_kinds.binding_kind as a deprecated alias for plugin
compatibility.
We also replace bool with implicit_status in a few places in the
codebase.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/constrexpr.mli | 8 | ||||
| -rw-r--r-- | intf/decl_kinds.mli | 5 | ||||
| -rw-r--r-- | intf/glob_term.mli | 6 |
3 files changed, 11 insertions, 8 deletions
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index 0cbb29575d..e494b2f81f 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -23,8 +23,8 @@ type explicitation = | ExplByName of Id.t type binder_kind = - | Default of binding_kind - | Generalized of binding_kind * binding_kind * bool + | Default of implicit_status + | Generalized of implicit_status * implicit_status * bool (** Inner binding, outer bindings, typeclass-specific flag for implicit generalization of superclasses *) @@ -95,7 +95,7 @@ and constr_expr = | CSort of Loc.t * glob_sort | CCast of Loc.t * constr_expr * constr_expr cast_type | CNotation of Loc.t * notation * constr_notation_substitution - | CGeneralization of Loc.t * binding_kind * abstraction_kind option * constr_expr + | CGeneralization of Loc.t * implicit_status * abstraction_kind option * constr_expr | CPrim of Loc.t * prim_token | CDelimiters of Loc.t * string * constr_expr @@ -132,7 +132,7 @@ and constr_notation_substitution = constr_expr list list * (** for recursive notations *) local_binder list list (** for binders subexpressions *) -type typeclass_constraint = (Name.t located * Id.t located list option) * binding_kind * constr_expr +type typeclass_constraint = (Name.t located * Id.t located list option) * implicit_status * constr_expr and typeclass_context = typeclass_constraint list diff --git a/intf/decl_kinds.mli b/intf/decl_kinds.mli index 29972f2f46..c117baf3f3 100644 --- a/intf/decl_kinds.mli +++ b/intf/decl_kinds.mli @@ -10,7 +10,10 @@ type locality = Discharge | Local | Global -type binding_kind = Explicit | Implicit +type implicit_status = Explicit | Implicit + +type binding_kind = implicit_status +(** @deprecated Alias type *) type polymorphic = bool diff --git a/intf/glob_term.mli b/intf/glob_term.mli index b3159c860c..178952fef1 100644 --- a/intf/glob_term.mli +++ b/intf/glob_term.mli @@ -40,8 +40,8 @@ type glob_constr = | GEvar of Loc.t * existential_name * (Id.t * glob_constr) list | GPatVar of Loc.t * (bool * patvar) (** Used for patterns only *) | GApp of Loc.t * glob_constr * glob_constr list - | GLambda of Loc.t * Name.t * binding_kind * glob_constr * glob_constr - | GProd of Loc.t * Name.t * binding_kind * glob_constr * glob_constr + | GLambda of Loc.t * Name.t * implicit_status * glob_constr * glob_constr + | GProd of Loc.t * Name.t * implicit_status * glob_constr * glob_constr | GLetIn of Loc.t * Name.t * glob_constr * glob_constr | GCases of Loc.t * case_style * glob_constr option * tomatch_tuples * cases_clauses (** [GCases(l,style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in [MatchStyle]) *) @@ -54,7 +54,7 @@ type glob_constr = | GHole of (Loc.t * Evar_kinds.t * intro_pattern_naming_expr * Genarg.glob_generic_argument option) | GCast of Loc.t * glob_constr * glob_constr cast_type -and glob_decl = Name.t * binding_kind * glob_constr option * glob_constr +and glob_decl = Name.t * implicit_status * glob_constr option * glob_constr and fix_recursion_order = | GStructRec |