aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-03-11 20:29:16 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-03-28 14:16:52 +0200
commit0ade32f84b28d2190360ec79520788142755b5b7 (patch)
tree46b2d11c817707c3b84653b490de3b0aaad42038 /kernel
parentbd8606189268c3fcdd3506872d459cb9032a33bf (diff)
[api] Deprecate a couple of aliases that we missed.
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cClosure.ml4
-rw-r--r--kernel/cClosure.mli4
-rw-r--r--kernel/constr.ml2
-rw-r--r--kernel/constr.mli6
-rw-r--r--kernel/environ.mli2
-rw-r--r--kernel/names.mli19
-rw-r--r--kernel/term.ml2
-rw-r--r--kernel/term.mli6
-rw-r--r--kernel/typeops.mli4
9 files changed, 26 insertions, 23 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 5f683790c..08114abc4 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -96,7 +96,7 @@ module type RedFlagsSig = sig
val red_transparent : reds -> transparent_state
val mkflags : red_kind list -> reds
val red_set : reds -> red_kind -> bool
- val red_projection : reds -> projection -> bool
+ val red_projection : reds -> Projection.t -> bool
end
module RedFlags = (struct
@@ -364,7 +364,7 @@ and fterm =
| FInd of pinductive
| FConstruct of pconstructor
| FApp of fconstr * fconstr array
- | FProj of projection * fconstr
+ | FProj of Projection.t * fconstr
| FFix of fixpoint * fconstr subs
| FCoFix of cofixpoint * fconstr subs
| FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 3a7f77d52..e2f5a3b82 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -74,7 +74,7 @@ module type RedFlagsSig = sig
(** This tests if the projection is in unfolded state already or
is unfodable due to delta. *)
- val red_projection : reds -> projection -> bool
+ val red_projection : reds -> Projection.t -> bool
end
module RedFlags : RedFlagsSig
@@ -132,7 +132,7 @@ type fterm =
| FInd of inductive Univ.puniverses
| FConstruct of constructor Univ.puniverses
| FApp of fconstr * fconstr array
- | FProj of projection * fconstr
+ | FProj of Projection.t * fconstr
| FFix of fixpoint * fconstr subs
| FCoFix of cofixpoint * fconstr subs
| FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
diff --git a/kernel/constr.ml b/kernel/constr.ml
index ba7fecadf..4f062d72f 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -100,7 +100,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
| Case of case_info * 'constr * 'constr * 'constr array
| Fix of ('constr, 'types) pfixpoint
| CoFix of ('constr, 'types) pcofixpoint
- | Proj of projection * 'constr
+ | Proj of Projection.t * 'constr
(* constr is the fixpoint of the previous type. Requires option
-rectypes of the Caml compiler to be set *)
type t = (t, t, Sorts.t, Instance.t) kind_of_term
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 98c0eaa28..0d464840c 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -122,7 +122,7 @@ val mkConst : Constant.t -> constr
val mkConstU : pconstant -> constr
(** Constructs a projection application *)
-val mkProj : (projection * constr) -> constr
+val mkProj : (Projection.t * constr) -> constr
(** Inductive types *)
@@ -220,7 +220,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
| Case of case_info * 'constr * 'constr * 'constr array
| Fix of ('constr, 'types) pfixpoint
| CoFix of ('constr, 'types) pcofixpoint
- | Proj of projection * 'constr
+ | Proj of Projection.t * 'constr
(** User view of [constr]. For [App], it is ensured there is at
least one argument and the function is not itself an applicative
@@ -318,7 +318,7 @@ where [info] is pretty-printing information *)
val destCase : constr -> case_info * constr * constr * constr array
(** Destructs a projection *)
-val destProj : constr -> projection * constr
+val destProj : constr -> Projection.t * constr
(** Destructs the {% $ %}i{% $ %}th function of the block
[Fixpoint f{_ 1} ctx{_ 1} = b{_ 1}
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 4e6ac1e72..fdd84b25b 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -168,7 +168,7 @@ val constant_opt_value_in : env -> Constant.t puniverses -> constr option
(** {6 Primitive projections} *)
-val lookup_projection : Names.projection -> env -> projection_body
+val lookup_projection : Names.Projection.t -> env -> projection_body
val is_projection : Constant.t -> env -> bool
(** {5 Inductive types } *)
diff --git a/kernel/names.mli b/kernel/names.mli
index ffd96781b..96e020aed 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -547,6 +547,8 @@ val eq_constant_key : Constant.t -> Constant.t -> bool
(** equalities on constant and inductive names (for the checker) *)
val eq_con_chk : Constant.t -> Constant.t -> bool
+[@@ocaml.deprecated "Same as [Constant.UserOrd.equal]."]
+
val eq_ind_chk : inductive -> inductive -> bool
(** {6 Deprecated functions. For backward compatibility.} *)
@@ -633,27 +635,27 @@ val eq_label : Label.t -> Label.t -> bool
(** {5 Unique bound module names} *)
type mod_bound_id = MBId.t
-(** Alias type. *)
+[@@ocaml.deprecated "Same as [MBId.t]."]
-val mod_bound_id_ord : mod_bound_id -> mod_bound_id -> int
+val mod_bound_id_ord : MBId.t -> MBId.t -> int
[@@ocaml.deprecated "Same as [MBId.compare]."]
-val mod_bound_id_eq : mod_bound_id -> mod_bound_id -> bool
+val mod_bound_id_eq : MBId.t -> MBId.t -> bool
[@@ocaml.deprecated "Same as [MBId.equal]."]
-val make_mbid : DirPath.t -> Id.t -> mod_bound_id
+val make_mbid : DirPath.t -> Id.t -> MBId.t
[@@ocaml.deprecated "Same as [MBId.make]."]
-val repr_mbid : mod_bound_id -> int * Id.t * DirPath.t
+val repr_mbid : MBId.t -> int * Id.t * DirPath.t
[@@ocaml.deprecated "Same as [MBId.repr]."]
-val id_of_mbid : mod_bound_id -> Id.t
+val id_of_mbid : MBId.t -> Id.t
[@@ocaml.deprecated "Same as [MBId.to_id]."]
-val string_of_mbid : mod_bound_id -> string
+val string_of_mbid : MBId.t -> string
[@@ocaml.deprecated "Same as [MBId.to_string]."]
-val debug_string_of_mbid : mod_bound_id -> string
+val debug_string_of_mbid : MBId.t -> string
[@@ocaml.deprecated "Same as [MBId.debug_to_string]."]
(** {5 Names} *)
@@ -745,6 +747,7 @@ module Projection : sig
end
type projection = Projection.t
+[@@ocaml.deprecated "Alias for [Projection.t]"]
val constant_of_kn_equiv : KerName.t -> KerName.t -> Constant.t
[@@ocaml.deprecated "Same as [Constant.make]"]
diff --git a/kernel/term.ml b/kernel/term.ml
index 403ed881c..e1affb1c0 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -92,7 +92,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
| Case of case_info * 'constr * 'constr * 'constr array
| Fix of ('constr, 'types) pfixpoint
| CoFix of ('constr, 'types) pcofixpoint
- | Proj of projection * 'constr
+ | Proj of Projection.t * 'constr
type values = Vmvalues.values
diff --git a/kernel/term.mli b/kernel/term.mli
index 7cb3b662d..ee84dcb2b 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -155,7 +155,7 @@ val destCase : constr -> case_info * constr * constr * constr array
[@@ocaml.deprecated "Alias for [Constr.destCase]"]
(** Destructs a projection *)
-val destProj : constr -> projection * constr
+val destProj : constr -> Projection.t * constr
[@@ocaml.deprecated "Alias for [Constr.destProj]"]
(** Destructs the {% $ %}i{% $ %}th function of the block
@@ -403,7 +403,7 @@ val mkApp : constr * constr array -> constr
[@@ocaml.deprecated "Alias for Constr"]
val mkConst : Constant.t -> constr
[@@ocaml.deprecated "Alias for Constr"]
-val mkProj : projection * constr -> constr
+val mkProj : Projection.t * constr -> constr
[@@ocaml.deprecated "Alias for Constr"]
val mkInd : inductive -> constr
[@@ocaml.deprecated "Alias for Constr"]
@@ -571,7 +571,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
| Case of Constr.case_info * 'constr * 'constr * 'constr array
| Fix of ('constr, 'types) Constr.pfixpoint
| CoFix of ('constr, 'types) Constr.pcofixpoint
- | Proj of projection * 'constr
+ | Proj of Projection.t * 'constr
[@@ocaml.deprecated "Alias for Constr.kind_of_term"]
type values = Vmvalues.values
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index bff40b017..85b2cfffd 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -60,7 +60,7 @@ val judge_of_constant : env -> pconstant -> unsafe_judgment
(** {6 type of an applied projection } *)
-val judge_of_projection : env -> Names.projection -> unsafe_judgment -> unsafe_judgment
+val judge_of_projection : env -> Projection.t -> unsafe_judgment -> unsafe_judgment
(** {6 Type of application. } *)
val judge_of_apply :
@@ -100,7 +100,7 @@ val judge_of_case : env -> case_info
-> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array
-> unsafe_judgment
-val type_of_projection_constant : env -> Names.projection puniverses -> types
+val type_of_projection_constant : env -> Projection.t puniverses -> types
val type_of_constant_in : env -> pconstant -> types