aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cemitcodes.ml4
-rw-r--r--kernel/declarations.mli23
-rw-r--r--kernel/declareops.ml2
-rw-r--r--kernel/inductive.ml2
-rw-r--r--kernel/mod_typing.ml128
-rw-r--r--kernel/mod_typing.mli24
-rw-r--r--kernel/modops.ml7
-rw-r--r--kernel/modops.mli5
-rw-r--r--kernel/names.mli10
-rw-r--r--kernel/nativelambda.ml2
-rw-r--r--kernel/nativevalues.ml27
-rw-r--r--kernel/pre_env.mli1
-rw-r--r--kernel/safe_typing.ml9
-rw-r--r--kernel/term.ml11
-rw-r--r--kernel/term_typing.ml13
-rw-r--r--kernel/uGraph.ml10
16 files changed, 131 insertions, 147 deletions
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 5ba93eda05..61042ccc17 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -306,8 +306,6 @@ let init () =
type emitcodes = string
-let copy = String.copy
-
let length = String.length
type to_patch = emitcodes * (patch list) * fv
@@ -332,8 +330,6 @@ let subst_patch s (ri,pos) =
let subst_to_patch s (code,pl,fv) =
code,List.rev_map (subst_patch s) pl,fv
-let subst_pconstant s (kn, u) = (fst (subst_con_kn s kn), u)
-
type body_code =
| BCdefined of to_patch
| BCalias of Names.constant
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 981dfe05ef..ebf12bd60d 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -237,17 +237,26 @@ and module_body =
{ mod_mp : module_path; (** absolute path of the module *)
mod_expr : module_implementation; (** implementation *)
mod_type : module_signature; (** expanded type *)
- (** algebraic type, kept if it's relevant for extraction *)
- mod_type_alg : module_expression option;
- (** set of all universes constraints in the module *)
- mod_constraints : Univ.ContextSet.t;
- (** quotiented set of equivalent constants and inductive names *)
- mod_delta : Mod_subst.delta_resolver;
+ mod_type_alg : module_expression option; (** algebraic type *)
+ mod_constraints : Univ.ContextSet.t; (**
+ set of all universes constraints in the module *)
+ mod_delta : Mod_subst.delta_resolver; (**
+ quotiented set of equivalent constants and inductive names *)
mod_retroknowledge : Retroknowledge.action list }
+(** For a module, there are five possible situations:
+ - [Declare Module M : T] then [mod_expr = Abstract; mod_type_alg = Some T]
+ - [Module M := E] then [mod_expr = Algebraic E; mod_type_alg = None]
+ - [Module M : T := E] then [mod_expr = Algebraic E; mod_type_alg = Some T]
+ - [Module M. ... End M] then [mod_expr = FullStruct; mod_type_alg = None]
+ - [Module M : T. ... End M] then [mod_expr = Struct; mod_type_alg = Some T]
+ And of course, all these situations may be functors or not. *)
+
(** A [module_type_body] is just a [module_body] with no
implementation ([mod_expr] always [Abstract]) and also
- an empty [mod_retroknowledge] *)
+ an empty [mod_retroknowledge]. Its [mod_type_alg] contains
+ the algebraic definition of this module type, or [None]
+ if it has been built interactively. *)
and module_type_body = module_body
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 6239d3c8d6..cc11b98c3d 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -391,5 +391,3 @@ and hcons_module_body mb =
mod_delta = delta';
mod_retroknowledge = retroknowledge';
}
-
-and hcons_module_type_body mtb = hcons_module_body mtb
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index f9a6e04c12..7bf1bfeb2d 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -150,7 +150,7 @@ let remember_subst u subst =
(* Bind expected levels of parameters to actual levels *)
(* Propagate the new levels in the signature *)
-let rec make_subst env =
+let make_subst env =
let rec make subst = function
| (_,Some _,_)::sign, exp, args ->
make subst (sign, exp, args)
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 3c58e788c7..3a75a74d91 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -21,7 +21,7 @@ open Modops
open Mod_subst
type 'alg translation =
- module_signature * 'alg option * delta_resolver * Univ.ContextSet.t
+ module_signature * 'alg * delta_resolver * Univ.ContextSet.t
let rec mp_from_mexpr = function
| MEident mp -> mp
@@ -183,8 +183,11 @@ let rec check_with_mod env struc (idl,mp1) mp equiv =
begin
try
let mtb_old = module_type_of_module old in
- Univ.ContextSet.add_constraints (Subtyping.check_subtypes env' mtb_mp1 mtb_old) old.mod_constraints
- with Failure _ -> error_incorrect_with_constraint lab
+ let chk_cst = Subtyping.check_subtypes env' mtb_mp1 mtb_old in
+ Univ.ContextSet.add_constraints chk_cst old.mod_constraints
+ with Failure _ ->
+ (* TODO: where can a Failure come from ??? *)
+ error_incorrect_with_constraint lab
end
| Algebraic (NoFunctor (MEident(mp'))) ->
check_modpath_equiv env' mp1 mp';
@@ -238,104 +241,89 @@ let rec check_with_mod env struc (idl,mp1) mp equiv =
| Not_found -> error_no_such_label lab
| Reduction.NotConvertible -> error_incorrect_with_constraint lab
-let mk_alg_with alg wd = Option.map (fun a -> MEwith (a,wd)) alg
-
let check_with env mp (sign,alg,reso,cst) = function
|WithDef(idl,c) ->
let struc = destr_nofunctor sign in
let struc',c',cst' = check_with_def env struc (idl,c) mp reso in
- let alg' = mk_alg_with alg (WithDef (idl,(c',Univ.ContextSet.to_context cst'))) in
- (NoFunctor struc'),alg',reso, cst+++cst'
+ let wd' = WithDef (idl,(c',Univ.ContextSet.to_context cst')) in
+ NoFunctor struc', MEwith (alg,wd'), reso, cst+++cst'
|WithMod(idl,mp1) as wd ->
let struc = destr_nofunctor sign in
let struc',reso',cst' = check_with_mod env struc (idl,mp1) mp reso in
- let alg' = mk_alg_with alg wd in
- (NoFunctor struc'),alg',reso', cst+++cst'
+ NoFunctor struc', MEwith (alg,wd), reso', cst+++cst'
-let mk_alg_app mpo alg arg = match mpo, alg with
- | Some _, Some alg -> Some (MEapply (alg,arg))
- | _ -> None
+let translate_apply env inl (sign,alg,reso,cst1) mp1 mkalg =
+ let farg_id, farg_b, fbody_b = destr_functor sign in
+ let mtb = module_type_of_module (lookup_module mp1 env) in
+ let cst2 = Subtyping.check_subtypes env mtb farg_b in
+ let mp_delta = discr_resolver mtb in
+ let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta in
+ let subst = map_mbid farg_id mp1 mp_delta in
+ let body = subst_signature subst fbody_b in
+ let alg' = mkalg alg mp1 in
+ let reso' = subst_codom_delta_resolver subst reso in
+ body,alg',reso', Univ.ContextSet.add_constraints cst2 cst1
(** Translation of a module struct entry :
- We translate to a module when a [module_path] is given,
otherwise to a module type.
- The first output is the expanded signature
- The second output is the algebraic expression, kept for the extraction.
- It is never None when translating to a module, but for module type
- it could not be contain [SEBapply] or [SEBfunctor].
*)
+let mk_alg_app alg arg = MEapply (alg,arg)
+
let rec translate_mse env mpo inl = function
- |MEident mp1 ->
- let sign,reso = match mpo with
- |Some mp ->
- let mb = strengthen_and_subst_mb (lookup_module mp1 env) mp false in
- mb.mod_type, mb.mod_delta
- |None ->
- let mtb = lookup_modtype mp1 env in
- mtb.mod_type, mtb.mod_delta
+ |MEident mp1 as me ->
+ let mb = match mpo with
+ |Some mp -> strengthen_and_subst_mb (lookup_module mp1 env) mp false
+ |None -> lookup_modtype mp1 env
in
- sign,Some (MEident mp1),reso,Univ.ContextSet.empty
+ mb.mod_type, me, mb.mod_delta, Univ.ContextSet.empty
|MEapply (fe,mp1) ->
- translate_apply env inl (translate_mse env mpo inl fe) mp1 (mk_alg_app mpo)
+ translate_apply env inl (translate_mse env mpo inl fe) mp1 mk_alg_app
|MEwith(me, with_decl) ->
assert (mpo == None); (* No 'with' syntax for modules *)
let mp = mp_from_mexpr me in
check_with env mp (translate_mse env None inl me) with_decl
-and translate_apply env inl (sign,alg,reso,cst1) mp1 mkalg =
- let farg_id, farg_b, fbody_b = destr_functor sign in
- let mtb = module_type_of_module (lookup_module mp1 env) in
- let cst2 = Subtyping.check_subtypes env mtb farg_b in
- let mp_delta = discr_resolver mtb in
- let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta in
- let subst = map_mbid farg_id mp1 mp_delta in
- let body = subst_signature subst fbody_b in
- let alg' = mkalg alg mp1 in
- let reso' = subst_codom_delta_resolver subst reso in
- body,alg',reso', Univ.ContextSet.add_constraints cst2 cst1
-
-let mk_alg_funct mpo mbid mtb alg = match mpo, alg with
- | Some _, Some alg -> Some (MoreFunctor (mbid,mtb,alg))
- | _ -> None
-
-let mk_mod mp e ty ty' cst reso =
+let mk_mod mp e ty cst reso =
{ mod_mp = mp;
mod_expr = e;
mod_type = ty;
- mod_type_alg = ty';
+ mod_type_alg = None;
mod_constraints = cst;
mod_delta = reso;
mod_retroknowledge = [] }
-let mk_modtype mp ty cst reso = mk_mod mp Abstract ty None cst reso
+let mk_modtype mp ty cst reso = mk_mod mp Abstract ty cst reso
let rec translate_mse_funct env mpo inl mse = function
|[] ->
let sign,alg,reso,cst = translate_mse env mpo inl mse in
- sign, Option.map (fun a -> NoFunctor a) alg, reso, cst
+ sign, NoFunctor alg, reso, cst
|(mbid, ty) :: params ->
let mp_id = MPbound mbid in
let mtb = translate_modtype env mp_id inl ([],ty) in
let env' = add_module_type mp_id mtb env in
let sign,alg,reso,cst = translate_mse_funct env' mpo inl mse params in
- let alg' = mk_alg_funct mpo mbid mtb alg in
+ let alg' = MoreFunctor (mbid,mtb,alg) in
MoreFunctor (mbid, mtb, sign), alg',reso, cst +++ mtb.mod_constraints
and translate_modtype env mp inl (params,mte) =
let sign,alg,reso,cst = translate_mse_funct env None inl mte params in
let mtb = mk_modtype (mp_from_mexpr mte) sign cst reso in
let mtb' = subst_modtype_and_resolver mtb mp in
- { mtb' with mod_type_alg = alg }
+ { mtb' with mod_type_alg = Some alg }
(** [finalize_module] :
- from an already-translated (or interactive) implementation
- and a signature entry, produce a final [module_expr] *)
+ from an already-translated (or interactive) implementation and
+ an (optional) signature entry, produces a final [module_body] *)
let finalize_module env mp (sign,alg,reso,cst) restype = match restype with
|None ->
let impl = match alg with Some e -> Algebraic e | None -> FullStruct in
- mk_mod mp impl sign None cst reso
+ mk_mod mp impl sign cst reso
|Some (params_mte,inl) ->
let res_mtb = translate_modtype env mp inl params_mte in
let auto_mtb = mk_modtype mp sign Univ.ContextSet.empty reso in
@@ -344,33 +332,59 @@ let finalize_module env mp (sign,alg,reso,cst) restype = match restype with
{ res_mtb with
mod_mp = mp;
mod_expr = impl;
- (** cst from module body typing, cst' from subtyping,
- and constraints from module type. *)
- mod_constraints = Univ.ContextSet.add_constraints cst' (cst +++ res_mtb.mod_constraints) }
+ (** cst from module body typing,
+ cst' from subtyping,
+ constraints from module type. *)
+ mod_constraints =
+ Univ.ContextSet.add_constraints cst' (cst +++ res_mtb.mod_constraints) }
let translate_module env mp inl = function
|MType (params,ty) ->
let mtb = translate_modtype env mp inl (params,ty) in
module_body_of_type mp mtb
|MExpr (params,mse,oty) ->
- let t = translate_mse_funct env (Some mp) inl mse params in
+ let (sg,alg,reso,cst) = translate_mse_funct env (Some mp) inl mse params in
let restype = Option.map (fun ty -> ((params,ty),inl)) oty in
- finalize_module env mp t restype
+ finalize_module env mp (sg,Some alg,reso,cst) restype
+
+(** We now forbid any Include of functors with restricted signatures.
+ Otherwise, we could end with the creation of undesired axioms
+ (see #3746). Note that restricted non-functorized modules are ok,
+ thanks to strengthening. *)
+
+let rec unfunct = function
+ |NoFunctor me -> me
+ |MoreFunctor(_,_,me) -> unfunct me
+
+let rec forbid_incl_signed_functor env = function
+ |MEapply(fe,_) -> forbid_incl_signed_functor env fe
+ |MEwith _ -> assert false (* No 'with' syntax for modules *)
+ |MEident mp1 ->
+ let mb = lookup_module mp1 env in
+ match mb.mod_type, mb.mod_type_alg, mb.mod_expr with
+ |MoreFunctor _, Some _, _ ->
+ (* functor + restricted signature = error *)
+ error_include_restricted_functor mp1
+ |MoreFunctor _, None, Algebraic me ->
+ (* functor, no signature yet, a definition which may be restricted *)
+ forbid_incl_signed_functor env (unfunct me)
+ |_ -> ()
let rec translate_mse_inclmod env mp inl = function
|MEident mp1 ->
let mb = strengthen_and_subst_mb (lookup_module mp1 env) mp true in
let sign = clean_bounded_mod_expr mb.mod_type in
- sign,None,mb.mod_delta,Univ.ContextSet.empty
+ sign,(),mb.mod_delta,Univ.ContextSet.empty
|MEapply (fe,arg) ->
let ftrans = translate_mse_inclmod env mp inl fe in
- translate_apply env inl ftrans arg (fun _ _ -> None)
+ translate_apply env inl ftrans arg (fun _ _ -> ())
|MEwith _ -> assert false (* No 'with' syntax for modules *)
let translate_mse_incl is_mod env mp inl me =
if is_mod then
+ let () = forbid_incl_signed_functor env me in
translate_mse_inclmod env mp inl me
else
let mtb = translate_modtype env mp inl ([],me) in
let sign = clean_bounded_mod_expr mtb.mod_type in
- sign,None,mtb.mod_delta,mtb.mod_constraints
+ sign,(),mtb.mod_delta,mtb.mod_constraints
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index bc0e20205a..d07d59dd9b 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -14,9 +14,18 @@ open Names
(** Main functions for translating module entries *)
+(** [translate_module] produces a [module_body] out of a [module_entry].
+ In the output fields:
+ - [mod_expr] is [Abstract] for a [MType] entry, or [Algebraic] for [MExpr].
+ - [mod_type_alg] is [None] only for a [MExpr] without explicit signature.
+*)
+
val translate_module :
env -> module_path -> inline -> module_entry -> module_body
+(** [translate_modtype] produces a [module_type_body] whose [mod_type_alg]
+ cannot be [None] (and of course [mod_expr] is [Abstract]). *)
+
val translate_modtype :
env -> module_path -> inline -> module_type_entry -> module_type_body
@@ -24,20 +33,21 @@ val translate_modtype :
- We translate to a module when a [module_path] is given,
otherwise to a module type.
- The first output is the expanded signature
- - The second output is the algebraic expression, kept for the extraction.
- It is never None when translating to a module, but for module type
- it could not be contain applications or functors.
-*)
+ - The second output is the algebraic expression, kept mostly for
+ the extraction. *)
type 'alg translation =
- module_signature * 'alg option * delta_resolver * Univ.ContextSet.t
+ module_signature * 'alg * delta_resolver * Univ.ContextSet.t
val translate_mse :
env -> module_path option -> inline -> module_struct_entry ->
module_alg_expr translation
+(** From an already-translated (or interactive) implementation and
+ an (optional) signature entry, produces a final [module_body] *)
+
val finalize_module :
- env -> module_path -> module_expression translation ->
+ env -> module_path -> (module_expression option) translation ->
(module_type_entry * inline) option ->
module_body
@@ -46,4 +56,4 @@ val finalize_module :
val translate_mse_incl :
bool -> env -> module_path -> inline -> module_struct_entry ->
- module_alg_expr translation
+ unit translation
diff --git a/kernel/modops.ml b/kernel/modops.ml
index cbb7963315..341c3993a3 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -67,15 +67,13 @@ type module_typing_error =
| IncorrectWithConstraint of Label.t
| GenerativeModuleExpected of Label.t
| LabelMissing of Label.t * string
+ | IncludeRestrictedFunctor of module_path
exception ModuleTypingError of module_typing_error
let error_existing_label l =
raise (ModuleTypingError (LabelAlreadyDeclared l))
-let error_application_to_not_path mexpr =
- raise (ModuleTypingError (ApplicationToNotPath mexpr))
-
let error_not_a_functor () =
raise (ModuleTypingError NotAFunctor)
@@ -112,6 +110,9 @@ let error_generative_module_expected l =
let error_no_such_label_sub l l1 =
raise (ModuleTypingError (LabelMissing (l,l1)))
+let error_include_restricted_functor mp =
+ raise (ModuleTypingError (IncludeRestrictedFunctor mp))
+
(** {6 Operations on functors } *)
let is_functor = function
diff --git a/kernel/modops.mli b/kernel/modops.mli
index a335ad9b4a..86aae598c2 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -126,13 +126,12 @@ type module_typing_error =
| IncorrectWithConstraint of Label.t
| GenerativeModuleExpected of Label.t
| LabelMissing of Label.t * string
+ | IncludeRestrictedFunctor of module_path
exception ModuleTypingError of module_typing_error
val error_existing_label : Label.t -> 'a
-val error_application_to_not_path : module_struct_entry -> 'a
-
val error_incompatible_modtypes :
module_type_body -> module_type_body -> 'a
@@ -152,3 +151,5 @@ val error_incorrect_with_constraint : Label.t -> 'a
val error_generative_module_expected : Label.t -> 'a
val error_no_such_label_sub : Label.t->string->'a
+
+val error_include_restricted_functor : module_path -> 'a
diff --git a/kernel/names.mli b/kernel/names.mli
index d424552e44..df296ab6c6 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -409,7 +409,7 @@ end
module Mindset : CSig.SetS with type elt = MutInd.t
module Mindmap : Map.ExtS with type key = MutInd.t and module Set := Mindset
-module Mindmap_env : Map.S with type key = MutInd.t
+module Mindmap_env : CSig.MapS with type key = MutInd.t
(** Designation of a (particular) inductive type. *)
type inductive = MutInd.t (* the name of the inductive type *)
@@ -422,10 +422,10 @@ type constructor = inductive (* designates the inductive type *)
* int (* the index of the constructor
BEWARE: indexing starts from 1. *)
-module Indmap : Map.S with type key = inductive
-module Constrmap : Map.S with type key = constructor
-module Indmap_env : Map.S with type key = inductive
-module Constrmap_env : Map.S with type key = constructor
+module Indmap : CSig.MapS with type key = inductive
+module Constrmap : CSig.MapS with type key = constructor
+module Indmap_env : CSig.MapS with type key = inductive
+module Constrmap_env : CSig.MapS with type key = constructor
val ind_modpath : inductive -> ModPath.t
val constr_modpath : constructor -> ModPath.t
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 4d033bc999..3ff9b5702c 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -485,7 +485,7 @@ module Renv =
let pop env = Vect.pop env.name_rel
let popn env n =
- for i = 1 to n do pop env done
+ for _i = 1 to n do pop env done
let get env n =
Lrel (Vect.get_last env.name_rel (n-1), n)
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 40bef4bc67..6e097b6133 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -78,8 +78,6 @@ let accumulate_code (k:accumulator) (x:t) =
let rec accumulate (x:t) =
accumulate_code (Obj.magic accumulate) x
-let raccumulate = ref accumulate
-
let mk_accu_gen rcode (a:atom) =
(* Format.eprintf "size rcode =%i\n" (Obj.size (Obj.magic rcode)); *)
let r = Obj.new_block 0 3 in
@@ -160,31 +158,6 @@ let is_accu x =
let o = Obj.repr x in
Obj.is_block o && Int.equal (Obj.tag o) accumulate_tag
-(*let accumulate_fix_code (k:accumulator) (a:t) =
- match atom_of_accu k with
- | Afix(frec,_,rec_pos,_,_) ->
- let nargs = accu_nargs k in
- if nargs <> rec_pos || is_accu a then
- accumulate_code k a
- else
- let r = ref frec in
- for i = 0 to nargs - 1 do
- r := !r (arg_of_accu k i)
- done;
- !r a
- | _ -> assert false
-
-
-let rec accumulate_fix (x:t) =
- accumulate_fix_code (Obj.magic accumulate_fix) x
-
-let raccumulate_fix = ref accumulate_fix *)
-
-let is_atom_fix (a:atom) =
- match a with
- | Afix _ -> true
- | _ -> false
-
let mk_fix_accu rec_pos pos types bodies =
mk_accu_gen accumulate (Afix(types,bodies,rec_pos, pos))
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 9cd940a881..1e95a3564d 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -9,7 +9,6 @@
open Names
open Term
open Declarations
-open Univ
(** The type of environments. *)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index f86fdfa971..33aa2972b2 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -222,13 +222,6 @@ let inline_private_constants_in_constr = Term_typing.inline_side_effects
let inline_private_constants_in_definition_entry = Term_typing.inline_entry_side_effects
let side_effects_of_private_constants x = Term_typing.uniq_seff (List.rev x)
-let constant_entry_of_private_constant = function
- | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } ->
- [ kn, Term_typing.constant_entry_of_side_effect cb eff_env ]
- | { Entries.eff = Entries.SEscheme (l,_) } ->
- List.map (fun (_,kn,cb,eff_env) ->
- kn, Term_typing.constant_entry_of_side_effect cb eff_env) l
-
let private_con_of_con env c =
let cbo = Environ.lookup_constant c env.env in
{ Entries.from_env = Ephemeron.create env.revstruct;
@@ -748,7 +741,7 @@ let end_modtype l senv =
let add_include me is_module inl senv =
let open Mod_typing in
let mp_sup = senv.modpath in
- let sign,_,resolver,cst =
+ let sign,(),resolver,cst =
translate_mse_incl is_module senv.env mp_sup inl me
in
let senv = add_constraints (Now (false, cst)) senv in
diff --git a/kernel/term.ml b/kernel/term.ml
index 19f4b7a234..24f82a9ec8 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -485,8 +485,6 @@ let lambda_applist c l =
let lambda_appvect c v = lambda_applist c (Array.to_list v)
-let lambda_app c a = lambda_applist c [a]
-
let lambda_applist_assum n c l =
let rec app n subst t l =
if Int.equal n 0 then
@@ -500,15 +498,6 @@ let lambda_applist_assum n c l =
let lambda_appvect_assum n c v = lambda_applist_assum n c (Array.to_list v)
-(* pseudo-reduction rule:
- * [prod_app s (Prod(_,B)) N --> B[N]
- * with an strip_outer_cast on the first argument to produce a product *)
-
-let prod_app t n =
- match kind_of_term (strip_outer_cast t) with
- | Prod (_,_,b) -> subst1 n b
- | _ -> anomaly (str"Needed a product, but didn't find one")
-
(* prod_applist T [ a1 ; ... ; an ] -> (T a1 ... an) *)
let prod_applist c l =
let rec app subst c l =
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index db50a393b5..a4e119f0b4 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -423,11 +423,16 @@ let export_side_effects mb env ce =
let trusted = check_signatures mb signatures in
let push_seff env = function
| kn, cb, `Nothing, _ ->
- Environ.add_constant kn cb env
+ let env = Environ.add_constant kn cb env in
+ if not cb.const_polymorphic then
+ Environ.push_context ~strict:true cb.const_universes env
+ else env
| kn, cb, `Opaque(_, ctx), _ ->
- let env = Environ.add_constant kn cb env in
- Environ.push_context_set
- ~strict:(not cb.const_polymorphic) ctx env in
+ let env = Environ.add_constant kn cb env in
+ if not cb.const_polymorphic then
+ let env = Environ.push_context ~strict:true cb.const_universes env in
+ Environ.push_context_set ~strict:true ctx env
+ else env in
let rec translate_seff sl seff acc env =
match sl, seff with
| _, [] -> List.rev acc, ce
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 9e8ffbc7f2..6765f91ee1 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -139,7 +139,6 @@ let rec repr g u =
| Equiv v -> repr g v
| Canonical arc -> arc
-let get_prop_arc g = repr g Level.prop
let get_set_arc g = repr g Level.set
let is_set_arc u = Level.is_set u.univ
let is_prop_arc u = Level.is_prop u.univ
@@ -155,7 +154,7 @@ let use_index g u =
(* [safe_repr] is like [repr] but if the graph doesn't contain the
searched universe, we add it. *)
-let rec safe_repr g u =
+let safe_repr g u =
let rec safe_repr_rec entries u =
match UMap.find u entries with
| Equiv v -> safe_repr_rec entries v
@@ -278,7 +277,7 @@ exception CycleDetected
problems. arXiv preprint arXiv:1112.0784. *)
(* [delta] is the timeout for backward search. It might be
- usefull to tune a multiplicative constant. *)
+ useful to tune a multiplicative constant. *)
let get_delta g =
int_of_float
(min (float_of_int g.n_edges ** 0.5)
@@ -669,7 +668,7 @@ let check_leq g u v =
is_type0m_univ u ||
check_eq_univs g u v || real_check_leq g u v
-(* enforc_univ_eq g u v will force u=v if possible, will fail otherwise *)
+(* enforce_univ_eq g u v will force u=v if possible, will fail otherwise *)
let rec enforce_univ_eq u v g =
let ucan = repr g u in
@@ -745,9 +744,6 @@ let check_constraints c g =
(* Normalization *)
-let lookup_level u g =
- try Some (UMap.find u g) with Not_found -> None
-
(** [normalize_universes g] returns a graph where all edges point
directly to the canonical representent of their target. The output
graph should be equivalent to the input graph from a logical point
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 01:40:15 +0000