aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrexpr_ops.ml8
-rw-r--r--interp/constrexpr_ops.mli4
-rw-r--r--interp/constrextern.ml4
-rw-r--r--interp/constrintern.ml2
-rw-r--r--interp/constrintern.mli2
-rw-r--r--interp/notation_ops.ml14
-rw-r--r--interp/notation_ops.mli2
-rw-r--r--intf/constrexpr.mli8
-rw-r--r--intf/decl_kinds.mli5
-rw-r--r--intf/glob_term.mli6
-rw-r--r--library/declare.ml6
-rw-r--r--library/declare.mli2
-rw-r--r--library/lib.ml4
-rw-r--r--library/lib.mli4
-rw-r--r--stm/lemmas.ml2
-rw-r--r--toplevel/command.ml2
-rw-r--r--toplevel/command.mli2
17 files changed, 40 insertions, 37 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 59c24900d..2644a56b3 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -17,7 +17,7 @@ open Decl_kinds
(***********************)
(* For binders parsing *)
-let binding_kind_eq bk1 bk2 = match bk1, bk2 with
+let implicit_status_eq bk1 bk2 = match bk1, bk2 with
| Explicit, Explicit -> true
| Implicit, Implicit -> true
| _ -> false
@@ -28,9 +28,9 @@ let abstraction_kind_eq ak1 ak2 = match ak1, ak2 with
| _ -> false
let binder_kind_eq b1 b2 = match b1, b2 with
-| Default bk1, Default bk2 -> binding_kind_eq bk1 bk2
+| Default bk1, Default bk2 -> implicit_status_eq bk1 bk2
| Generalized (bk1, ck1, b1), Generalized (bk2, ck2, b2) ->
- binding_kind_eq bk1 bk2 && binding_kind_eq ck1 ck2 &&
+ implicit_status_eq bk1 bk2 && implicit_status_eq ck1 ck2 &&
(if b1 then b2 else not b2)
| _ -> false
@@ -165,7 +165,7 @@ let rec constr_expr_eq e1 e2 =
| CPrim(_,i1), CPrim(_,i2) ->
prim_token_eq i1 i2
| CGeneralization (_, bk1, ak1, e1), CGeneralization (_, bk2, ak2, e2) ->
- binding_kind_eq bk1 bk2 &&
+ implicit_status_eq bk1 bk2 &&
Option.equal abstraction_kind_eq ak1 ak2 &&
constr_expr_eq e1 e2
| CDelimiters(_,s1,e1), CDelimiters(_,s2,e2) ->
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index a92da035f..bfe546ba5 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -26,8 +26,8 @@ val constr_expr_eq : constr_expr -> constr_expr -> bool
val local_binder_eq : local_binder -> local_binder -> bool
(** Equality on [local_binder]. Same properties as [constr_expr_eq]. *)
-val binding_kind_eq : Decl_kinds.binding_kind -> Decl_kinds.binding_kind -> bool
-(** Equality on [binding_kind] *)
+val implicit_status_eq : Decl_kinds.implicit_status -> Decl_kinds.implicit_status -> bool
+(** Equality on [implicit_status] *)
val binder_kind_eq : binder_kind -> binder_kind -> bool
(** Equality on [binder_kind] *)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index f7fcbb4ee..62cb62f49 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -808,7 +808,7 @@ and factorize_prod scopes vars na bk aty c =
let c = extern_typ scopes vars c in
match na, c with
| Name id, CProdN (loc,[nal,Default bk',ty],c)
- when binding_kind_eq bk bk' && constr_expr_eq aty ty
+ when implicit_status_eq bk bk' && constr_expr_eq aty ty
&& not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) ->
nal,c
| _ ->
@@ -818,7 +818,7 @@ and factorize_lambda inctx scopes vars na bk aty c =
let c = sub_extern inctx scopes vars c in
match c with
| CLambdaN (loc,[nal,Default bk',ty],c)
- when binding_kind_eq bk bk' && constr_expr_eq aty ty
+ when implicit_status_eq bk bk' && constr_expr_eq aty ty
&& not (occur_name na ty) (* avoid na in ty escapes scope *) ->
nal,c
| _ ->
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index fb11359e3..b9f5704d8 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -65,7 +65,7 @@ type var_internalization_data =
type internalization_env =
(var_internalization_data) Id.Map.t
-type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr)
+type glob_binder = (Name.t * implicit_status * glob_constr option * glob_constr)
type ltac_sign = {
ltac_vars : Id.Set.t;
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index eea76aa31..718aa753e 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -75,7 +75,7 @@ type ltac_sign = {
val empty_ltac_sign : ltac_sign
-type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr)
+type glob_binder = (Name.t * implicit_status * glob_constr option * glob_constr)
(** {6 Internalization performs interpretation of global names and notations } *)
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 6b29b6d3d..c65d43db3 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -29,10 +29,10 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with
| GVar (_,v1), GVar (_,v2) -> on_true_do (Id.equal v1 v2) add (Name v1)
| GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 && List.for_all2eq f l1 l2
| GLambda (_,na1,bk1,ty1,c1), GLambda (_,na2,bk2,ty2,c2)
- when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
+ when Name.equal na1 na2 && Constrexpr_ops.implicit_status_eq bk1 bk2 ->
on_true_do (f ty1 ty2 && f c1 c2) add na1
| GProd (_,na1,bk1,ty1,c1), GProd (_,na2,bk2,ty2,c2)
- when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
+ when Name.equal na1 na2 && Constrexpr_ops.implicit_status_eq bk1 bk2 ->
on_true_do (f ty1 ty2 && f c1 c2) add na1
| GHole _, GHole _ -> true
| GSort (_,s1), GSort (_,s2) -> Miscops.glob_sort_eq s1 s2
@@ -772,18 +772,18 @@ let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma)
| GHole _, _ -> v'
| _, GHole _ -> v
| _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v else raise No_match in
- let unify_binding_kind bk bk' = if bk == bk' then bk' else raise No_match in
+ let unify_implicit_status bk bk' = if bk == bk' then bk' else raise No_match in
let unify_binder alp b b' =
match b, b' with
| (Inl na, bk, None, t), (Inl na', bk', None, t') (* assum *) ->
let alp, na = unify_name alp na na' in
- alp, (Inl na, unify_binding_kind bk bk', None, unify_term alp t t')
+ alp, (Inl na, unify_implicit_status bk bk', None, unify_term alp t t')
| (Inl na, bk, Some c, t), (Inl na', bk', Some c', t') (* let *) ->
let alp, na = unify_name alp na na' in
- alp, (Inl na, unify_binding_kind bk bk', Some (unify_term alp c c'), unify_term alp t t')
+ alp, (Inl na, unify_implicit_status bk bk', Some (unify_term alp c c'), unify_term alp t t')
| (Inr p, bk, None, t), (Inr p', bk', None, t') (* pattern *) ->
let alp, p = unify_pat alp p p' in
- alp, (Inr p, unify_binding_kind bk bk', None, unify_term alp t t')
+ alp, (Inr p, unify_implicit_status bk bk', None, unify_term alp t t')
| _ -> raise No_match in
let rec unify alp bl bl' =
match bl, bl' with
@@ -1122,7 +1122,7 @@ let term_of_binder = function
| Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)
type glob_decl2 =
- (name, cases_pattern) Util.union * Decl_kinds.binding_kind *
+ (name, cases_pattern) Util.union * Decl_kinds.implicit_status *
glob_constr option * glob_constr
let match_notation_constr u c (metas,pat) =
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 854e222e3..6428ccab6 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -48,7 +48,7 @@ val glob_constr_of_notation_constr : Loc.t -> notation_constr -> glob_constr
exception No_match
type glob_decl2 =
- (name, cases_pattern) Util.union * Decl_kinds.binding_kind *
+ (name, cases_pattern) Util.union * Decl_kinds.implicit_status *
glob_constr option * glob_constr
val match_notation_constr : bool -> glob_constr -> interpretation ->
(glob_constr * subscopes) list * (glob_constr list * subscopes) list *
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index 0cbb29575..e494b2f81 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 29972f2f4..c117baf3f 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 b3159c860..178952fef 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
diff --git a/library/declare.ml b/library/declare.ml
index 36a58629e..5c6543e28 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -46,7 +46,7 @@ type section_variable_entry =
| SectionLocalDef of Safe_typing.private_constants definition_entry
| SectionLocalAssum of { type_context : types Univ.in_universe_context_set;
polymorphic : bool;
- binding_kind : binding_kind }
+ implicit_status : implicit_status }
type variable_declaration = DirPath.t * section_variable_entry * logical_kind
@@ -59,9 +59,9 @@ let cache_variable ((sp,_),o) =
alreadydeclared (pr_id id ++ str " already exists");
let impl,opaque,polymorphic,ctx = match d with (* Fails if not well-typed *)
- | SectionLocalAssum { type_context = (ty,ctx); polymorphic; binding_kind } ->
+ | SectionLocalAssum { type_context = (ty,ctx); polymorphic; implicit_status } ->
let () = Global.push_named_assum ((id,ty,polymorphic),ctx) in
- binding_kind, true, polymorphic, ctx
+ implicit_status, true, polymorphic, ctx
| SectionLocalDef (de) ->
let univs = Global.push_named_def (id,de) in
Explicit, de.const_entry_opaque,
diff --git a/library/declare.mli b/library/declare.mli
index 760bf437b..a0ec26444 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -25,7 +25,7 @@ type section_variable_entry =
| SectionLocalDef of Safe_typing.private_constants definition_entry
| SectionLocalAssum of { type_context : types Univ.in_universe_context_set;
polymorphic : bool;
- binding_kind : binding_kind }
+ implicit_status : implicit_status }
type variable_declaration = DirPath.t * section_variable_entry * logical_kind
diff --git a/library/lib.ml b/library/lib.ml
index 954889fb6..13921610d 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -391,7 +391,7 @@ let find_opening_node id =
- the list of substitution to do at section closing
*)
-type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind
+type variable_info = Context.Named.Declaration.t * Decl_kinds.implicit_status
type variable_context = variable_info list
type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t
@@ -399,7 +399,7 @@ type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t
type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t
type secentry =
- | Variable of (Names.Id.t * Decl_kinds.binding_kind *
+ | Variable of (Names.Id.t * Decl_kinds.implicit_status *
Decl_kinds.polymorphic * Univ.universe_context_set)
| Context of Univ.universe_context_set
diff --git a/library/lib.mli b/library/lib.mli
index e905ee57e..51c74d395 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -162,7 +162,7 @@ val xml_open_section : (Names.Id.t -> unit) Hook.t
val xml_close_section : (Names.Id.t -> unit) Hook.t
(** {6 Section management for discharge } *)
-type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind
+type variable_info = Context.Named.Declaration.t * Decl_kinds.implicit_status
type variable_context = variable_info list
type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t
@@ -176,7 +176,7 @@ val variable_section_segment_of_reference : Globnames.global_reference -> variab
val section_instance : Globnames.global_reference -> Univ.universe_instance * Names.Id.t array
val is_in_section : Globnames.global_reference -> bool
-val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> polymorphic:bool -> Univ.universe_context_set -> unit
+val add_section_variable : Names.Id.t -> Decl_kinds.implicit_status -> polymorphic:bool -> Univ.universe_context_set -> unit
val add_section_context : Univ.universe_context_set -> unit
val add_section_constant : polymorphic:bool ->
Names.constant -> Context.Named.t -> unit
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 004dd6801..b1b8aa288 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -241,7 +241,7 @@ let save_remaining_recthms { locality; polymorphic; object_kind }
let k = IsAssumption Conjectural in
let c = SectionLocalAssum { type_context = (t_i,ctx);
polymorphic;
- binding_kind = impl }
+ implicit_status = impl }
in
let _ = declare_variable id (Lib.cwd(),c,k) in
(Discharge, VarRef id,imps)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 40c65b56f..7bb016d34 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -230,7 +230,7 @@ let declare_assumption is_coe assumption_kind (c,ctx) pl imps impl nl (_,ident)
| Discharge when Lib.sections_are_opened () ->
let entry = SectionLocalAssum { type_context = (c,ctx);
polymorphic;
- binding_kind = impl }
+ implicit_status = impl }
in
let decl = (Lib.cwd(), entry, IsAssumption kind) in
let _ = declare_variable ident decl in
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 2ae4cddd0..f0651a98c 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -55,7 +55,7 @@ val do_definition : Id.t -> definition_kind -> lident list option ->
val declare_assumption : coercion_flag -> assumption_kind ->
types Univ.in_universe_context_set ->
Universes.universe_binders -> Impargs.manual_implicits ->
- binding_kind -> Vernacexpr.inline -> variable Loc.located ->
+ implicit_status -> Vernacexpr.inline -> variable Loc.located ->
global_reference * Univ.Instance.t * bool
val do_assumptions : assumption_kind ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 07:27:11 +0000