aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cClosure.ml10
-rw-r--r--kernel/cClosure.mli1
-rw-r--r--kernel/constr.mli8
-rw-r--r--kernel/cooking.ml40
-rw-r--r--kernel/environ.mli2
-rw-r--r--kernel/mod_subst.ml28
-rw-r--r--kernel/modops.ml14
-rw-r--r--kernel/names.ml59
-rw-r--r--kernel/names.mli29
-rw-r--r--kernel/nativecode.ml2
-rw-r--r--kernel/nativelibrary.ml2
-rw-r--r--kernel/reduction.ml2
-rw-r--r--kernel/safe_typing.ml34
-rw-r--r--kernel/safe_typing.mli7
-rw-r--r--kernel/subtyping.ml4
-rw-r--r--kernel/term_typing.ml6
-rw-r--r--kernel/term_typing.mli2
-rw-r--r--kernel/uGraph.mli2
-rw-r--r--kernel/univ.ml12
-rw-r--r--kernel/univ.mli56
20 files changed, 89 insertions, 231 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 003b49535f..819a66c190 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -359,7 +359,6 @@ type fconstr = {
and fterm =
| FRel of int
| FAtom of constr (* Metas and Sorts *)
- | FCast of fconstr * cast_kind * fconstr
| FFlex of table_key
| FInd of pinductive
| FConstruct of pconstructor
@@ -477,7 +476,7 @@ let rec lft_fconstr n ft =
| FCoFix(cfx,e) -> {norm=Cstr; term=FCoFix(cfx,subs_shft(n,e))}
| FLIFT(k,m) -> lft_fconstr (n+k) m
| FLOCKED -> assert false
- | FFlex _ | FAtom _ | FCast _ | FApp _ | FProj _ | FCaseT _ | FProd _
+ | FFlex _ | FAtom _ | FApp _ | FProj _ | FCaseT _ | FProd _
| FLetIn _ | FEvar _ | FCLOS _ -> {norm=ft.norm; term=FLIFT(n,ft)}
let lift_fconstr k f =
if Int.equal k 0 then f else lft_fconstr k f
@@ -558,8 +557,6 @@ let rec to_constr lfts v =
| FFlex (RelKey p) -> mkRel (reloc_rel p lfts)
| FFlex (VarKey x) -> mkVar x
| FAtom c -> exliftn lfts c
- | FCast (a,k,b) ->
- mkCast (to_constr lfts a, k, to_constr lfts b)
| FFlex (ConstKey op) -> mkConstU op
| FInd op -> mkIndU op
| FConstruct op -> mkConstructU op
@@ -866,7 +863,6 @@ let rec knh info m stk =
(match get_nth_arg m ri.(n) stk with
(Some(pars,arg),stk') -> knh info arg (Zfix(m,pars)::stk')
| (None, stk') -> (m,stk'))
- | FCast(t,_,_) -> knh info t stk
| FProj (p,c) ->
(match unfold_projection info p with
| None -> (m, stk)
@@ -951,7 +947,7 @@ let rec knr info tab m stk =
(match evar_value info.i_cache ev with
Some c -> knit info tab env c stk
| None -> (m,stk))
- | FLOCKED | FRel _ | FAtom _ | FCast _ | FFlex _ | FInd _ | FApp _ | FProj _
+ | FLOCKED | FRel _ | FAtom _ | FFlex _ | FInd _ | FApp _ | FProj _
| FFix _ | FCoFix _ | FCaseT _ | FLambda _ | FProd _ | FLetIn _ | FLIFT _
| FCLOS _ -> (m, stk)
@@ -1031,7 +1027,7 @@ and norm_head info tab m =
mkEvar(i, Array.map (fun a -> kl info tab (mk_clos env a)) args)
| FProj (p,c) ->
mkProj (p, kl info tab c)
- | FLOCKED | FRel _ | FAtom _ | FCast _ | FFlex _ | FInd _ | FConstruct _
+ | FLOCKED | FRel _ | FAtom _ | FFlex _ | FInd _ | FConstruct _
| FApp _ | FCaseT _ | FLIFT _ | FCLOS _ -> term_of_fconstr m
(* Initialization and then normalization *)
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 6121b3a1ec..2a018d172a 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -131,7 +131,6 @@ type fconstr
type fterm =
| FRel of int
| FAtom of constr (** Metas and Sorts *)
- | FCast of fconstr * cast_kind * fconstr
| FFlex of table_key
| FInd of inductive Univ.puniverses
| FConstruct of constructor Univ.puniverses
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 2efdae007c..3c9cc96a0d 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -13,20 +13,12 @@
open Names
-(** {6 Value under universe substitution } *)
-type 'a puniverses = 'a Univ.puniverses
-[@@ocaml.deprecated "use Univ.puniverses"]
-
(** {6 Simply type aliases } *)
type pconstant = Constant.t Univ.puniverses
type pinductive = inductive Univ.puniverses
type pconstructor = constructor Univ.puniverses
(** {6 Existential variables } *)
-type existential_key = Evar.t
-[@@ocaml.deprecated "use Evar.t"]
-
-(** {6 Existential variables } *)
type metavariable = int
(** {6 Case annotation } *)
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index b361e36bbf..b39aed01e8 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -15,7 +15,6 @@
(* This module implements kernel-level discharching of local
declarations over global constants and inductive types *)
-open CErrors
open Util
open Names
open Term
@@ -28,18 +27,6 @@ module RelDecl = Context.Rel.Declaration
(*s Cooking the constants. *)
-let pop_dirpath p = match DirPath.repr p with
- | [] -> anomaly ~label:"dirpath_prefix" (Pp.str "empty dirpath.")
- | _::l -> DirPath.make l
-
-let pop_mind kn =
- let (mp,dir,l) = MutInd.repr3 kn in
- MutInd.make3 mp (pop_dirpath dir) l
-
-let pop_con con =
- let (mp,dir,l) = Constant.repr3 con in
- Constant.make3 mp (pop_dirpath dir) l
-
type my_global_reference =
| ConstRef of Constant.t
| IndRef of inductive
@@ -71,29 +58,26 @@ let instantiate_my_gr gr u =
let share cache r (cstl,knl) =
try RefTable.find cache r
with Not_found ->
- let f,(u,l) =
+ let (u,l) =
match r with
- | IndRef (kn,i) ->
- IndRef (pop_mind kn,i), Mindmap.find kn knl
- | ConstructRef ((kn,i),j) ->
- ConstructRef ((pop_mind kn,i),j), Mindmap.find kn knl
+ | IndRef (kn,_i) ->
+ Mindmap.find kn knl
+ | ConstructRef ((kn,_i),_j) ->
+ Mindmap.find kn knl
| ConstRef cst ->
- ConstRef (pop_con cst), Cmap.find cst cstl in
- let c = (f, (u, Array.map mkVar l)) in
+ Cmap.find cst cstl in
+ let c = (u, Array.map mkVar l) in
RefTable.add cache r c;
c
let share_univs cache r u l =
- let r', (u', args) = share cache r l in
- mkApp (instantiate_my_gr r' (Instance.append u' u), args)
+ let (u', args) = share cache r l in
+ mkApp (instantiate_my_gr r (Instance.append u' u), args)
let update_case_info cache ci modlist =
try
- let ind, n =
- match share cache (IndRef ci.ci_ind) modlist with
- | (IndRef f,(_u,l)) -> (f, Array.length l)
- | _ -> assert false in
- { ci with ci_ind = ind; ci_npar = ci.ci_npar + n }
+ let (_u,l) = share cache (IndRef ci.ci_ind) modlist in
+ { ci with ci_npar = ci.ci_npar + Array.length l }
with Not_found ->
ci
@@ -129,7 +113,7 @@ let expmod_constr cache modlist c =
| Proj (p, c') ->
let map cst npars =
let _, newpars = Mindmap.find cst (snd modlist) in
- pop_mind cst, npars + Array.length newpars
+ (cst, npars + Array.length newpars)
in
let p' = try Projection.map_npars map p with Not_found -> p in
let c'' = substrec c' in
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 1343b9029b..55ff7ff162 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -320,8 +320,6 @@ val remove_hyps : Id.Set.t -> (Constr.named_declaration -> Constr.named_declarat
open Retroknowledge
(** functions manipulating the retroknowledge
@author spiwack *)
-val retroknowledge : (retroknowledge->'a) -> env -> 'a
-[@@ocaml.deprecated "Use the record projection."]
val registered : env -> field -> bool
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index bff3092655..2a91c7dab0 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -173,12 +173,12 @@ let solve_delta_kn resolve kn =
| Inline (lev, Some c) -> raise (Change_equiv_to_inline (lev,c))
| Inline (_, None) -> raise Not_found
with Not_found ->
- let mp,dir,l = KerName.repr kn in
+ let mp,l = KerName.repr kn in
let new_mp = find_prefix resolve mp in
if mp == new_mp then
kn
else
- KerName.make new_mp dir l
+ KerName.make new_mp l
let kn_of_delta resolve kn =
try solve_delta_kn resolve kn
@@ -245,18 +245,18 @@ let subst_mp sub mp =
| Some (mp',_) -> mp'
let subst_kn_delta sub kn =
- let mp,dir,l = KerName.repr kn in
+ let mp,l = KerName.repr kn in
match subst_mp0 sub mp with
Some (mp',resolve) ->
- solve_delta_kn resolve (KerName.make mp' dir l)
+ solve_delta_kn resolve (KerName.make mp' l)
| None -> kn
let subst_kn sub kn =
- let mp,dir,l = KerName.repr kn in
+ let mp,l = KerName.repr kn in
match subst_mp0 sub mp with
Some (mp',_) ->
- (KerName.make mp' dir l)
+ (KerName.make mp' l)
| None -> kn
exception No_subst
@@ -275,12 +275,12 @@ let progress f x ~orelse =
if y != x then y else orelse
let subst_mind sub mind =
- let mpu,dir,l = MutInd.repr3 mind in
+ let mpu,l = MutInd.repr2 mind in
let mpc = KerName.modpath (MutInd.canonical mind) in
try
let mpu,mpc,resolve,user = subst_dual_mp sub mpu mpc in
- let knu = KerName.make mpu dir l in
- let knc = if mpu == mpc then knu else KerName.make mpc dir l in
+ let knu = KerName.make mpu l in
+ let knc = if mpu == mpc then knu else KerName.make mpc l in
let knc' =
progress (kn_of_delta resolve) (if user then knu else knc) ~orelse:knc
in
@@ -295,11 +295,11 @@ let subst_pind sub (ind,u) =
(subst_ind sub ind, u)
let subst_con0 sub (cst,u) =
- let mpu,dir,l = Constant.repr3 cst in
+ let mpu,l = Constant.repr2 cst in
let mpc = KerName.modpath (Constant.canonical cst) in
let mpu,mpc,resolve,user = subst_dual_mp sub mpu mpc in
- let knu = KerName.make mpu dir l in
- let knc = if mpu == mpc then knu else KerName.make mpc dir l in
+ let knu = KerName.make mpu l in
+ let knc = if mpu == mpc then knu else KerName.make mpc l in
match search_delta_inline resolve knu knc with
| Some (ctx, t) ->
(* In case of inlining, discard the canonical part (cf #2608) *)
@@ -433,10 +433,10 @@ let rec replace_mp_in_mp mpfrom mpto mp =
| _ -> mp
let replace_mp_in_kn mpfrom mpto kn =
- let mp,dir,l = KerName.repr kn in
+ let mp,l = KerName.repr kn in
let mp'' = replace_mp_in_mp mpfrom mpto mp in
if mp==mp'' then kn
- else KerName.make mp'' dir l
+ else KerName.make mp'' l
let rec mp_in_mp mp mp1 =
match mp1 with
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 424d329e09..bab2eae3df 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -289,10 +289,10 @@ let add_retroknowledge =
let rec add_structure mp sign resolver linkinfo env =
let add_one env (l,elem) = match elem with
|SFBconst cb ->
- let c = constant_of_delta_kn resolver (KerName.make2 mp l) in
+ let c = constant_of_delta_kn resolver (KerName.make mp l) in
Environ.add_constant_key c cb linkinfo env
|SFBmind mib ->
- let mind = mind_of_delta_kn resolver (KerName.make2 mp l) in
+ let mind = mind_of_delta_kn resolver (KerName.make mp l) in
let mib =
if mib.mind_private != None then
{ mib with mind_private = Some true }
@@ -331,7 +331,7 @@ let strengthen_const mp_from l cb resolver =
match cb.const_body with
|Def _ -> cb
|_ ->
- let kn = KerName.make2 mp_from l in
+ let kn = KerName.make mp_from l in
let con = constant_of_delta_kn resolver kn in
let u =
match cb.const_universes with
@@ -450,8 +450,8 @@ and strengthen_and_subst_struct str subst mp_from mp_to alias incl reso =
(* If we are performing an inclusion we need to add
the fact that the constant mp_to.l is \Delta-equivalent
to reso(mp_from.l) *)
- let kn_from = KerName.make2 mp_from l in
- let kn_to = KerName.make2 mp_to l in
+ let kn_from = KerName.make mp_from l in
+ let kn_to = KerName.make mp_to l in
let old_name = kn_of_delta reso kn_from in
add_kn_delta_resolver kn_to old_name reso', str'
else
@@ -471,8 +471,8 @@ and strengthen_and_subst_struct str subst mp_from mp_to alias incl reso =
in
(* Same as constant *)
if incl then
- let kn_from = KerName.make2 mp_from l in
- let kn_to = KerName.make2 mp_to l in
+ let kn_from = KerName.make mp_from l in
+ let kn_to = KerName.make mp_to l in
let old_name = kn_of_delta reso kn_from in
add_kn_delta_resolver kn_to old_name reso', str'
else
diff --git a/kernel/names.ml b/kernel/names.ml
index 6d33f233e9..7cd749de1d 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -365,7 +365,6 @@ module KerName = struct
type t = {
modpath : ModPath.t;
- dirpath : DirPath.t;
knlabel : Label.t;
mutable refhash : int;
(** Lazily computed hash. If unset, it is set to negative values. *)
@@ -373,22 +372,18 @@ module KerName = struct
type kernel_name = t
- let make modpath dirpath knlabel =
- { modpath; dirpath; knlabel; refhash = -1; }
- let repr kn = (kn.modpath, kn.dirpath, kn.knlabel)
+ let make modpath knlabel =
+ { modpath; knlabel; refhash = -1; }
+ let repr kn = (kn.modpath, kn.knlabel)
- let make2 modpath knlabel =
- { modpath; dirpath = DirPath.empty; knlabel; refhash = -1; }
+ let make2 = make
+ [@@ocaml.deprecated "Please use [KerName.make]"]
let modpath kn = kn.modpath
let label kn = kn.knlabel
let to_string_gen mp_to_string kn =
- let dp =
- if DirPath.is_empty kn.dirpath then "."
- else "#" ^ DirPath.to_string kn.dirpath ^ "#"
- in
- mp_to_string kn.modpath ^ dp ^ Label.to_string kn.knlabel
+ mp_to_string kn.modpath ^ "." ^ Label.to_string kn.knlabel
let to_string kn = to_string_gen ModPath.to_string kn
@@ -402,9 +397,7 @@ module KerName = struct
let c = String.compare kn1.knlabel kn2.knlabel in
if not (Int.equal c 0) then c
else
- let c = DirPath.compare kn1.dirpath kn2.dirpath in
- if not (Int.equal c 0) then c
- else ModPath.compare kn1.modpath kn2.modpath
+ ModPath.compare kn1.modpath kn2.modpath
let equal kn1 kn2 =
let h1 = kn1.refhash in
@@ -412,7 +405,6 @@ module KerName = struct
if 0 <= h1 && 0 <= h2 && not (Int.equal h1 h2) then false
else
Label.equal kn1.knlabel kn2.knlabel &&
- DirPath.equal kn1.dirpath kn2.dirpath &&
ModPath.equal kn1.modpath kn2.modpath
open Hashset.Combine
@@ -420,8 +412,8 @@ module KerName = struct
let hash kn =
let h = kn.refhash in
if h < 0 then
- let { modpath = mp; dirpath = dp; knlabel = lbl; _ } = kn in
- let h = combine3 (ModPath.hash mp) (DirPath.hash dp) (Label.hash lbl) in
+ let { modpath = mp; knlabel = lbl; _ } = kn in
+ let h = combine (ModPath.hash mp) (Label.hash lbl) in
(* Ensure positivity on all platforms. *)
let h = h land 0x3FFFFFFF in
let () = kn.refhash <- h in
@@ -432,12 +424,11 @@ module KerName = struct
type t = kernel_name
type u = (ModPath.t -> ModPath.t) * (DirPath.t -> DirPath.t)
* (string -> string)
- let hashcons (hmod,hdir,hstr) kn =
- let { modpath = mp; dirpath = dp; knlabel = l; refhash; } = kn in
- { modpath = hmod mp; dirpath = hdir dp; knlabel = hstr l; refhash; }
+ let hashcons (hmod,_hdir,hstr) kn =
+ let { modpath = mp; knlabel = l; refhash; } = kn in
+ { modpath = hmod mp; knlabel = hstr l; refhash; }
let eq kn1 kn2 =
- kn1.modpath == kn2.modpath && kn1.dirpath == kn2.dirpath &&
- kn1.knlabel == kn2.knlabel
+ kn1.modpath == kn2.modpath && kn1.knlabel == kn2.knlabel
let hash = hash
end
@@ -492,21 +483,20 @@ module KerPair = struct
let make knu knc = if KerName.equal knu knc then Same knc else Dual (knu,knc)
let make1 = same
- let make2 mp l = same (KerName.make2 mp l)
- let make3 mp dir l = same (KerName.make mp dir l)
- let repr3 kp = KerName.repr (user kp)
+ let make2 mp l = same (KerName.make mp l)
+ let repr2 kp = KerName.repr (user kp)
let label kp = KerName.label (user kp)
let modpath kp = KerName.modpath (user kp)
let change_label kp lbl =
- let (mp1,dp1,l1) = KerName.repr (user kp)
- and (mp2,dp2,l2) = KerName.repr (canonical kp) in
- assert (String.equal l1 l2 && DirPath.equal dp1 dp2);
+ let (mp1,l1) = KerName.repr (user kp)
+ and (mp2,l2) = KerName.repr (canonical kp) in
+ assert (String.equal l1 l2);
if String.equal lbl l1 then kp
else
- let kn = KerName.make mp1 dp1 lbl in
+ let kn = KerName.make mp1 lbl in
if mp1 == mp2 then same kn
- else make kn (KerName.make mp2 dp2 lbl)
+ else make kn (KerName.make mp2 lbl)
let to_string kp = KerName.to_string (user kp)
let print kp = str (to_string kp)
@@ -749,15 +739,12 @@ let eq_table_key f ik1 ik2 =
| RelKey k1, RelKey k2 -> Int.equal k1 k2
| _ -> false
-let eq_con_chk = Constant.UserOrd.equal
let eq_mind_chk = MutInd.UserOrd.equal
let eq_ind_chk (kn1,i1) (kn2,i2) = Int.equal i1 i2 && eq_mind_chk kn1 kn2
-
(*******************************************************************)
(** Compatibility layers *)
-type mod_bound_id = MBId.t
let eq_constant_key = Constant.UserOrd.equal
(** Compatibility layer for [ModPath] *)
@@ -933,8 +920,6 @@ struct
end
-type projection = Projection.t
-
module GlobRefInternal = struct
type t =
@@ -1025,10 +1010,6 @@ module GlobRef = struct
end
-type global_reference = GlobRef.t
-[@@ocaml.deprecated "Alias for [GlobRef.t]"]
-
-
type evaluable_global_reference =
| EvalVarRef of Id.t
| EvalConstRef of Constant.t
diff --git a/kernel/names.mli b/kernel/names.mli
index 2ea8108734..37930c12e2 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -274,9 +274,11 @@ sig
type t
(** Constructor and destructor *)
- val make : ModPath.t -> DirPath.t -> Label.t -> t
+ val make : ModPath.t -> Label.t -> t
+ val repr : t -> ModPath.t * Label.t
+
val make2 : ModPath.t -> Label.t -> t
- val repr : t -> ModPath.t * DirPath.t * Label.t
+ [@@ocaml.deprecated "Please use [KerName.make]"]
(** Projections *)
val modpath : t -> ModPath.t
@@ -317,15 +319,12 @@ sig
val make2 : ModPath.t -> Label.t -> t
(** Shortcut for [(make1 (KerName.make2 ...))] *)
- val make3 : ModPath.t -> DirPath.t -> Label.t -> t
- (** Shortcut for [(make1 (KerName.make ...))] *)
-
(** Projections *)
val user : t -> KerName.t
val canonical : t -> KerName.t
- val repr3 : t -> ModPath.t * DirPath.t * Label.t
+ val repr2 : t -> ModPath.t * Label.t
(** Shortcut for [KerName.repr (user ...)] *)
val modpath : t -> ModPath.t
@@ -403,15 +402,12 @@ sig
val make2 : ModPath.t -> Label.t -> t
(** Shortcut for [(make1 (KerName.make2 ...))] *)
- val make3 : ModPath.t -> DirPath.t -> Label.t -> t
- (** Shortcut for [(make1 (KerName.make ...))] *)
-
(** Projections *)
val user : t -> KerName.t
val canonical : t -> KerName.t
- val repr3 : t -> ModPath.t * DirPath.t * Label.t
+ val repr2 : t -> ModPath.t * Label.t
(** Shortcut for [KerName.repr (user ...)] *)
val modpath : t -> ModPath.t
@@ -531,15 +527,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.} *)
-
-type mod_bound_id = MBId.t
-[@@ocaml.deprecated "Same as [MBId.t]."]
(** {5 Module paths} *)
type module_path = ModPath.t =
@@ -629,9 +618,6 @@ module Projection : sig
end
-type projection = Projection.t
-[@@ocaml.deprecated "Alias for [Projection.t]"]
-
(** {6 Global reference is a kernel side type for all references together } *)
(* XXX: Should we define GlobRefCan GlobRefUser? *)
@@ -669,9 +655,6 @@ module GlobRef : sig
end
-type global_reference = GlobRef.t
-[@@ocaml.deprecated "Alias for [GlobRef.t]"]
-
(** Better to have it here that in Closure, since required in grammar.cma *)
(* XXX: Move to a module *)
type evaluable_global_reference =
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 74b075f4a5..482a2f3a3c 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1561,7 +1561,7 @@ let rec list_of_mp acc = function
let list_of_mp mp = list_of_mp [] mp
let string_of_kn kn =
- let (mp,_dp,l) = KerName.repr kn in
+ let (mp,l) = KerName.repr kn in
let mp = list_of_mp mp in
String.concat "_" mp ^ "_" ^ string_of_label l
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index 8ac3538fc5..5d1b882361 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -27,7 +27,7 @@ let rec translate_mod prefix mp env mod_expr acc =
and translate_field prefix mp env acc (l,x) =
match x with
| SFBconst cb ->
- let con = Constant.make3 mp DirPath.empty l in
+ let con = Constant.make2 mp l in
(if !Flags.debug then
let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in
Feedback.msg_debug (Pp.str msg));
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 2abb4b485c..00576476ab 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -605,7 +605,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
(* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *)
| ( (FLetIn _, _) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_)
| (_, FLetIn _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _)
- | (FLOCKED,_) | (_,FLOCKED) ) | (FCast _, _) | (_, FCast _) -> assert false
+ | (FLOCKED,_) | (_,FLOCKED) ) -> assert false
| (FRel _ | FAtom _ | FInd _ | FFix _ | FCoFix _
| FProd _ | FEvar _), _ -> raise NotConvertible
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index b036aa6a67..820c5b3a2b 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -479,10 +479,10 @@ type global_declaration =
type exported_private_constant =
Constant.t * Entries.side_effect_role
-let add_constant_aux no_section senv (kn, cb) =
- let l = pi3 (Constant.repr3 kn) in
+let add_constant_aux ~in_section senv (kn, cb) =
+ let l = Constant.label kn in
let cb, otab = match cb.const_body with
- | OpaqueDef lc when no_section ->
+ | OpaqueDef lc when not in_section ->
(* In coqc, opaque constants outside sections will be stored
indirectly in a specific table *)
let od, otab =
@@ -505,13 +505,11 @@ let export_private_constants ~in_section ce senv =
let exported, ce = Term_typing.export_side_effects senv.revstruct senv.env ce in
let bodies = List.map (fun (kn, cb, _) -> (kn, cb)) exported in
let exported = List.map (fun (kn, _, r) -> (kn, r)) exported in
- let no_section = not in_section in
- let senv = List.fold_left (add_constant_aux no_section) senv bodies in
+ let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in
(ce, exported), senv
-let add_constant dir l decl senv =
- let kn = Constant.make3 senv.modpath dir l in
- let no_section = DirPath.is_empty dir in
+let add_constant ~in_section l decl senv =
+ let kn = Constant.make2 senv.modpath l in
let senv =
let cb =
match decl with
@@ -520,9 +518,9 @@ let add_constant dir l decl senv =
| ConstantEntry (PureEntry, ce) ->
Term_typing.translate_constant Term_typing.Pure senv.env kn ce
| GlobalRecipe r ->
- let cb = Term_typing.translate_recipe senv.env kn r in
- if no_section then Declareops.hcons_const_body cb else cb in
- add_constant_aux no_section senv (kn, cb) in
+ let cb = Term_typing.translate_recipe ~hcons:(not in_section) senv.env kn r in
+ if in_section then cb else Declareops.hcons_const_body cb in
+ add_constant_aux ~in_section senv (kn, cb) in
kn, senv
(** Insertion of inductive types *)
@@ -535,9 +533,9 @@ let check_mind mie lab =
(* The label and the first inductive type name should match *)
assert (Id.equal (Label.to_id lab) oie.mind_entry_typename)
-let add_mind dir l mie senv =
+let add_mind l mie senv =
let () = check_mind mie l in
- let kn = MutInd.make3 senv.modpath dir l in
+ let kn = MutInd.make2 senv.modpath l in
let mib = Term_typing.translate_mind senv.env kn mie in
let mib =
match mib.mind_hyps with [] -> Declareops.hcons_mind mib | _ -> mib
@@ -770,9 +768,9 @@ let add_include me is_module inl senv =
let add senv ((l,elem) as field) =
let new_name = match elem with
| SFBconst _ ->
- C (Mod_subst.constant_of_delta_kn resolver (KerName.make2 mp_sup l))
+ C (Mod_subst.constant_of_delta_kn resolver (KerName.make mp_sup l))
| SFBmind _ ->
- I (Mod_subst.mind_of_delta_kn resolver (KerName.make2 mp_sup l))
+ I (Mod_subst.mind_of_delta_kn resolver (KerName.make mp_sup l))
| SFBmodule _ -> M
| SFBmodtype _ -> MT
in
@@ -885,12 +883,6 @@ let typing senv = Typeops.infer (env_of_senv senv)
(** {6 Retroknowledge / native compiler } *)
-[@@@ocaml.warning "-3"]
-(** universal lifting, used for the "get" operations mostly *)
-let retroknowledge f senv =
- Environ.retroknowledge f (env_of_senv senv)
-[@@@ocaml.warning "+3"]
-
let register field value senv =
(* todo : value closed *)
(* spiwack : updates the safe_env with the information that the register
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 6e0febaa3f..0f150ea971 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -105,13 +105,13 @@ val export_private_constants : in_section:bool ->
(** returns the main constant plus a list of auxiliary constants (empty
unless one requires the side effects to be exported) *)
val add_constant :
- DirPath.t -> Label.t -> global_declaration ->
+ in_section:bool -> Label.t -> global_declaration ->
Constant.t safe_transformer
(** Adding an inductive type *)
val add_mind :
- DirPath.t -> Label.t -> Entries.mutual_inductive_entry ->
+ Label.t -> Entries.mutual_inductive_entry ->
MutInd.t safe_transformer
(** Adding a module or a module type *)
@@ -208,9 +208,6 @@ val delta_of_senv :
open Retroknowledge
-val retroknowledge : (retroknowledge-> 'a) -> safe_environment -> 'a
-[@@ocaml.deprecated "Use the projection of Environ.env"]
-
val register :
field -> GlobRef.t -> safe_transformer0
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index bfe68671a2..d64342dbb0 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -103,8 +103,8 @@ let check_polymorphic_instance error env auctx1 auctx2 =
(* for now we do not allow reorderings *)
let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2=
- let kn1 = KerName.make2 mp1 l in
- let kn2 = KerName.make2 mp2 l in
+ let kn1 = KerName.make mp1 l in
+ let kn2 = KerName.make mp2 l in
let error why = error_signature_mismatch l spec2 why in
let check_conv why cst poly f = check_conv_error error why cst poly f in
let mib1 =
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 47247ff25e..5ccc23eefc 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -531,11 +531,7 @@ let translate_local_assum env t =
let t = Typeops.assumption_of_judgment env j in
t
-let translate_recipe env kn r =
- (** We only hashcons the term when outside of a section, otherwise this would
- be useless. It is detected by the dirpath of the constant being empty. *)
- let (_, dir, _) = Constant.repr3 kn in
- let hcons = DirPath.is_empty dir in
+let translate_recipe ~hcons env kn r =
build_constant_declaration kn env (Cooking.cook_constant ~hcons r)
let translate_local_def env _id centry =
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index b05e05e4dc..ab25090b00 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -64,7 +64,7 @@ val export_side_effects :
val translate_mind :
env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body
-val translate_recipe : env -> Constant.t -> Cooking.recipe -> constant_body
+val translate_recipe : hcons:bool -> env -> Constant.t -> Cooking.recipe -> constant_body
(** Internal functions, mentioned here for debug purpose only *)
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index 752bf76270..4336a22b8c 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -12,8 +12,6 @@ open Univ
(** {6 Graphs of universes. } *)
type t
-type universes = t
-[@@ocaml.deprecated "Use UGraph.t"]
type 'a check_function = t -> 'a -> 'a -> bool
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 61ad1d0a82..fa37834a23 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -574,11 +574,8 @@ struct
pp_std ++ prl u1 ++ pr_constraint_type op ++
prl u2 ++ fnl () ) c (str "")
- let universes_of c =
- fold (fun (u1, _op, u2) unvs -> LSet.add u2 (LSet.add u1 unvs)) c LSet.empty
end
-let universes_of_constraints = Constraint.universes_of
let empty_constraint = Constraint.empty
let union_constraint = Constraint.union
let eq_constraint = Constraint.equal
@@ -897,8 +894,6 @@ let subst_instance_constraints s csts =
(fun c csts -> Constraint.add (subst_instance_constraint s c) csts)
csts Constraint.empty
-type universe_instance = Instance.t
-
type 'a puniverses = 'a * Instance.t
let out_punivs (x, _y) = x
let in_punivs x = (x, Instance.empty)
@@ -955,7 +950,6 @@ struct
end
-type abstract_universe_context = AUContext.t
let hcons_abstract_universe_context = AUContext.hcons
(** Universe info for cumulative inductive types: A context of
@@ -997,12 +991,10 @@ struct
end
-type cumulativity_info = CumulativityInfo.t
let hcons_cumulativity_info = CumulativityInfo.hcons
module ACumulativityInfo = CumulativityInfo
-type abstract_cumulativity_info = ACumulativityInfo.t
let hcons_abstract_cumulativity_info = ACumulativityInfo.hcons
(** A set of universes with universe constraints.
@@ -1238,7 +1230,3 @@ let explain_universe_inconsistency prl (o,u,v,p) =
in
str "Cannot enforce" ++ spc() ++ pr_uni u ++ spc() ++
pr_rel o ++ spc() ++ pr_uni v ++ reason
-
-let compare_levels = Level.compare
-let eq_levels = Level.equal
-let equal_universes = Universe.equal
diff --git a/kernel/univ.mli b/kernel/univ.mli
index b68bbdf359..1aa53b8aa8 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -51,9 +51,6 @@ sig
val name : t -> (Names.DirPath.t * int) option
end
-type universe_level = Level.t
-[@@ocaml.deprecated "Use Level.t"]
-
(** Sets of universe levels *)
module LSet :
sig
@@ -63,9 +60,6 @@ sig
(** Pretty-printing *)
end
-type universe_set = LSet.t
-[@@ocaml.deprecated "Use LSet.t"]
-
module Universe :
sig
type t
@@ -130,9 +124,6 @@ sig
end
-type universe = Universe.t
-[@@ocaml.deprecated "Use Universe.t"]
-
(** Alias name. *)
val pr_uni : Universe.t -> Pp.t
@@ -171,9 +162,6 @@ module Constraint : sig
include Set.S with type elt = univ_constraint
end
-type constraints = Constraint.t
-[@@ocaml.deprecated "Use Constraint.t"]
-
val empty_constraint : Constraint.t
val union_constraint : Constraint.t -> Constraint.t -> Constraint.t
val eq_constraint : Constraint.t -> Constraint.t -> bool
@@ -301,9 +289,6 @@ sig
end
-type universe_instance = Instance.t
-[@@ocaml.deprecated "Use Instance.t"]
-
val enforce_eq_instances : Instance.t constraint_function
val enforce_eq_variance_instances : Variance.t array -> Instance.t constraint_function
@@ -340,9 +325,6 @@ sig
end
-type universe_context = UContext.t
-[@@ocaml.deprecated "Use UContext.t"]
-
module AUContext :
sig
type t
@@ -367,9 +349,6 @@ sig
end
-type abstract_universe_context = AUContext.t
-[@@ocaml.deprecated "Use AUContext.t"]
-
(** Universe info for cumulative inductive types: A context of
universe levels with universe constraints, representing local
universe variables and constraints, together with an array of
@@ -398,9 +377,6 @@ sig
val eq_constraints : t -> Instance.t constraint_function
end
-type cumulativity_info = CumulativityInfo.t
-[@@ocaml.deprecated "Use CumulativityInfo.t"]
-
module ACumulativityInfo :
sig
type t
@@ -411,11 +387,13 @@ sig
val eq_constraints : t -> Instance.t constraint_function
end
-type abstract_cumulativity_info = ACumulativityInfo.t
-[@@ocaml.deprecated "Use ACumulativityInfo.t"]
-
(** Universe contexts (as sets) *)
+(** A set of universes with universe Constraint.t.
+ We linearize the set to a list after typechecking.
+ Beware, representation could change.
+*)
+
module ContextSet :
sig
type t = LSet.t constrained
@@ -451,13 +429,6 @@ sig
val size : t -> int
end
-(** A set of universes with universe Constraint.t.
- We linearize the set to a list after typechecking.
- Beware, representation could change.
-*)
-type universe_context_set = ContextSet.t
-[@@ocaml.deprecated "Use ContextSet.t"]
-
(** A value in a universe context (resp. context set). *)
type 'a in_universe_context = 'a * UContext.t
type 'a in_universe_context_set = 'a * ContextSet.t
@@ -532,20 +503,3 @@ val hcons_abstract_universe_context : AUContext.t -> AUContext.t
val hcons_universe_context_set : ContextSet.t -> ContextSet.t
val hcons_cumulativity_info : CumulativityInfo.t -> CumulativityInfo.t
val hcons_abstract_cumulativity_info : ACumulativityInfo.t -> ACumulativityInfo.t
-
-(******)
-
-(* deprecated: use qualified names instead *)
-val compare_levels : Level.t -> Level.t -> int
-[@@ocaml.deprecated "Use Level.compare"]
-
-val eq_levels : Level.t -> Level.t -> bool
-[@@ocaml.deprecated "Use Level.equal"]
-
-(** deprecated: Equality of formal universe expressions. *)
-val equal_universes : Universe.t -> Universe.t -> bool
-[@@ocaml.deprecated "Use Universe.equal"]
-
-(** Universes of Constraint.t *)
-val universes_of_constraints : Constraint.t -> LSet.t
-[@@ocaml.deprecated "Use Constraint.universes_of"]
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 08:38:09 +0000