aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cbytegen.ml11
-rw-r--r--kernel/cbytegen.mli4
-rw-r--r--kernel/cemitcodes.ml9
-rw-r--r--kernel/cemitcodes.mli4
-rw-r--r--kernel/cooking.ml3
-rw-r--r--kernel/cooking.mli2
-rw-r--r--kernel/csymtable.ml5
-rw-r--r--kernel/entries.ml3
-rw-r--r--kernel/entries.mli3
-rw-r--r--kernel/environ.mli4
-rw-r--r--kernel/mod_typing.ml4
-rw-r--r--kernel/modops.ml2
-rw-r--r--kernel/term_typing.ml8
-rw-r--r--kernel/term_typing.mli4
14 files changed, 25 insertions, 41 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 9c00af5dff..337b907512 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -714,18 +714,13 @@ let compile env c =
Format.print_flush(); *)
init_code,!fun_code, Array.of_list fv
-let compile_constant_body env body opaque boxed =
+let compile_constant_body env body opaque =
if opaque then BCconstant
else match body with
| None -> BCconstant
| Some sb ->
let body = Declarations.force sb in
- if boxed then
- let res = compile env body in
- let to_patch = to_memory res in
- BCdefined(true, to_patch)
- else
- match kind_of_term body with
+ match kind_of_term body with
| Const kn' ->
(* we use the canonical name of the constant*)
let con= constant_of_kn (canonical_con kn') in
@@ -733,7 +728,7 @@ let compile_constant_body env body opaque boxed =
| _ ->
let res = compile env body in
let to_patch = to_memory res in
- BCdefined (false, to_patch)
+ BCdefined to_patch
(* spiwack: additional function which allow different part of compilation of the
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index bf9c0be263..403c1c7b5b 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -10,8 +10,8 @@ val compile : env -> constr -> bytecodes * bytecodes * fv
(** init, fun, fv *)
val compile_constant_body :
- env -> constr_substituted option -> bool -> bool -> body_code
- (** opaque *) (* boxed *)
+ env -> constr_substituted option -> bool -> body_code
+ (** opaque *)
(** spiwack: this function contains the information needed to perform
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 1138031c7a..277b343b24 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -331,12 +331,12 @@ let subst_to_patch s (code,pl,fv) =
code,List.rev_map (subst_patch s) pl,fv
type body_code =
- | BCdefined of bool * to_patch
+ | BCdefined of to_patch
| BCallias of constant
| BCconstant
let subst_body_code s = function
- | BCdefined (b,tp) -> BCdefined (b,subst_to_patch s tp)
+ | BCdefined tp -> BCdefined (subst_to_patch s tp)
| BCallias kn -> BCallias (fst (subst_con s kn))
| BCconstant -> BCconstant
@@ -348,11 +348,6 @@ let force = force subst_body_code
let subst_to_patch_subst = subst_substituted
-let is_boxed tps =
- match force tps with
- | BCdefined(b,_) -> b
- | _ -> false
-
let to_memory (init_code, fun_code, fv) =
init();
emit init_code;
diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli
index a8ecc82b41..43cebb4748 100644
--- a/kernel/cemitcodes.mli
+++ b/kernel/cemitcodes.mli
@@ -22,7 +22,7 @@ type to_patch = emitcodes * (patch list) * fv
val subst_to_patch : Mod_subst.substitution -> to_patch -> to_patch
type body_code =
- | BCdefined of bool*to_patch
+ | BCdefined of to_patch
| BCallias of constant
| BCconstant
@@ -33,8 +33,6 @@ val from_val : body_code -> to_patch_substituted
val force : to_patch_substituted -> body_code
-val is_boxed : to_patch_substituted -> bool
-
val subst_to_patch_subst : Mod_subst.substitution -> to_patch_substituted -> to_patch_substituted
val to_memory : bytecodes * bytecodes * fv -> to_patch
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index e4336683d1..d01398841c 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -137,5 +137,4 @@ let cook_constant env r =
let j = make_judge (force (Option.get body)) typ in
Typeops.make_polymorphic_if_constant_for_ind env j
in
- let boxed = Cemitcodes.is_boxed cb.const_body_code in
- (body, typ, cb.const_constraints, cb.const_opaque, boxed,false)
+ (body, typ, cb.const_constraints, cb.const_opaque, false)
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 0f604a4bee..09b42d0b12 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -24,7 +24,7 @@ type recipe = {
val cook_constant :
env -> recipe ->
constr_substituted option * constant_type * constraints * bool * bool
- * bool
+
(** {6 Utility functions used in module [Discharge]. } *)
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 983c1f26df..897cbf13a8 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -125,10 +125,9 @@ let rec slot_for_getglobal env kn =
with NotEvaluated ->
let pos =
match Cemitcodes.force cb.const_body_code with
- | BCdefined(boxed,(code,pl,fv)) ->
+ | BCdefined(code,pl,fv) ->
let v = eval_to_patch env (code,pl,fv) in
- if boxed then set_global_boxed kn v
- else set_global v
+ set_global v
| BCallias kn' -> slot_for_getglobal env kn'
| BCconstant -> set_global (val_of_constant kn) in
rk := Some pos;
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 714da03196..dbf802bb12 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -57,8 +57,7 @@ type mutual_inductive_entry = {
type definition_entry = {
const_entry_body : constr;
const_entry_type : types option;
- const_entry_opaque : bool;
- const_entry_boxed : bool}
+ const_entry_opaque : bool }
(* type and the inlining flag *)
type parameter_entry = types * bool
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 2ba3064550..d45e2bbdb8 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -53,8 +53,7 @@ type mutual_inductive_entry = {
type definition_entry = {
const_entry_body : constr;
const_entry_type : types option;
- const_entry_opaque : bool;
- const_entry_boxed : bool }
+ const_entry_opaque : bool }
type parameter_entry = types * bool (*inline flag*)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 078d70965d..f26d49dde4 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -190,8 +190,8 @@ type unsafe_type_judgment = {
(** {6 Compilation of global declaration } *)
val compile_constant_body :
- env -> constr_substituted option -> bool -> bool -> Cemitcodes.body_code
- (** opaque *) (* boxed *)
+ env -> constr_substituted option -> bool -> Cemitcodes.body_code
+ (** opaque *)
exception Hyp_not_found
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 5a3dade530..407ae73ca7 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -95,7 +95,7 @@ and check_with_aux_def env sign with_decl mp equiv =
let cb' = {cb with
const_body = body;
const_body_code = Cemitcodes.from_val
- (compile_constant_body env' body false false);
+ (compile_constant_body env' body false);
const_constraints = cst} in
SEBstruct(before@((l,SFBconst(cb'))::after)),cb',cst
| Some b ->
@@ -105,7 +105,7 @@ and check_with_aux_def env sign with_decl mp equiv =
let cb' = {cb with
const_body = body;
const_body_code = Cemitcodes.from_val
- (compile_constant_body env' body false false);
+ (compile_constant_body env' body false);
const_constraints = cst} in
SEBstruct(before@((l,SFBconst(cb'))::after)),cb',cst
end
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 9da2f49622..ce968b40ef 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -276,7 +276,7 @@ let strengthen_const env mp_from l cb resolver =
const_body = const_subs;
const_opaque = false;
const_body_code = Cemitcodes.from_val
- (compile_constant_body env const_subs false false)
+ (compile_constant_body env const_subs false)
}
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index f765dd77e9..432460d7d5 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -94,11 +94,11 @@ let infer_declaration env dcl =
let (j,cst) = infer env c.const_entry_body in
let (typ,cst) = constrain_type env j cst c.const_entry_type in
Some (Declarations.from_val j.uj_val), typ, cst,
- c.const_entry_opaque, c.const_entry_boxed, false
+ c.const_entry_opaque, false
| ParameterEntry (t,nl) ->
let (j,cst) = infer env t in
None, NonPolymorphicType (Typeops.assumption_of_judgment env j), cst,
- false, false, nl
+ false, nl
let global_vars_set_constant_type env = function
| NonPolymorphicType t -> global_vars_set env t
@@ -108,7 +108,7 @@ let global_vars_set_constant_type env = function
(fun t c -> Idset.union (global_vars_set env t) c))
ctx ~init:Idset.empty
-let build_constant_declaration env kn (body,typ,cst,op,boxed,inline) =
+let build_constant_declaration env kn (body,typ,cst,op,inline) =
let ids =
match body with
| None -> global_vars_set_constant_type env typ
@@ -117,7 +117,7 @@ let build_constant_declaration env kn (body,typ,cst,op,boxed,inline) =
(global_vars_set env (Declarations.force b))
(global_vars_set_constant_type env typ)
in
- let tps = Cemitcodes.from_val (compile_constant_body env body op boxed) in
+ let tps = Cemitcodes.from_val (compile_constant_body env body op) in
let hyps = keep_hyps env ids in
{ const_hyps = hyps;
const_body = body;
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 628aa93756..500858a59c 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -22,10 +22,10 @@ val translate_local_assum : env -> types ->
types * Univ.constraints
val infer_declaration : env -> constant_entry ->
- constr_substituted option * constant_type * constraints * bool * bool * bool
+ constr_substituted option * constant_type * constraints * bool * bool
val build_constant_declaration : env -> 'a ->
- constr_substituted option * constant_type * constraints * bool * bool * bool ->
+ constr_substituted option * constant_type * constraints * bool * bool ->
constant_body
val translate_constant : env -> constant -> constant_entry -> constant_body
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:18:58 +0000