aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--API/API.mli6
-rw-r--r--checker/cic.mli7
-rw-r--r--checker/mod_checking.ml2
-rw-r--r--checker/modops.ml4
-rw-r--r--checker/subtyping.ml2
-rw-r--r--checker/values.ml4
-rw-r--r--kernel/declarations.ml7
-rw-r--r--kernel/mod_typing.ml7
-rw-r--r--kernel/modops.ml8
-rw-r--r--kernel/safe_typing.ml6
-rw-r--r--kernel/subtyping.ml2
11 files changed, 37 insertions, 18 deletions
diff --git a/API/API.mli b/API/API.mli
index aa7f93bb2..2a60cd54a 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -1287,7 +1287,7 @@ sig
mod_type_alg : module_expression option;
mod_constraints : Univ.ContextSet.t;
mod_delta : Mod_subst.delta_resolver;
- mod_retroknowledge : Retroknowledge.action list
+ mod_retroknowledge : 'a module_retroknowledge;
}
and module_signature = (module_type_body,structure_body) functorize
and module_body = module_implementation generic_module_body
@@ -1298,6 +1298,10 @@ sig
| SFBmind of mutual_inductive_body
| SFBmodule of module_body
| SFBmodtype of module_type_body
+ and _ module_retroknowledge =
+ | ModBodyRK :
+ Retroknowledge.action list -> module_implementation module_retroknowledge
+ | ModTypeRK : unit module_retroknowledge
end
module Declareops :
diff --git a/checker/cic.mli b/checker/cic.mli
index 6724fa3f0..753fd0fc0 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -395,7 +395,7 @@ and 'a generic_module_body =
mod_constraints : Univ.ContextSet.t;
(** quotiented set of equivalent constants and inductive names *)
mod_delta : delta_resolver;
- mod_retroknowledge : action list }
+ mod_retroknowledge : 'a module_retroknowledge; }
and module_body = module_implementation generic_module_body
@@ -404,6 +404,11 @@ and module_body = module_implementation generic_module_body
and module_type_body = unit generic_module_body
+and _ module_retroknowledge =
+| ModBodyRK :
+ action list -> module_implementation module_retroknowledge
+| ModTypeRK : unit module_retroknowledge
+
(*************************************************************************)
(** {4 From safe_typing.ml} *)
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index de568e636..3c9e1cac5 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -75,7 +75,7 @@ let mk_mtb mp sign delta =
mod_type_alg = None;
mod_constraints = Univ.ContextSet.empty;
mod_delta = delta;
- mod_retroknowledge = []; }
+ mod_retroknowledge = ModTypeRK; }
let rec check_module env mp mb =
let (_:module_signature) =
diff --git a/checker/modops.ml b/checker/modops.ml
index 726988752..f0abc39ea 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -49,7 +49,7 @@ let destr_functor = function
| NoFunctor _ -> error_not_a_functor ()
let module_body_of_type mp mtb =
- { mtb with mod_mp = mp; mod_expr = Abstract }
+ { mtb with mod_mp = mp; mod_expr = Abstract; mod_retroknowledge = ModBodyRK [] }
let rec add_structure mp sign resolver env =
let add_one env (l,elem) =
@@ -142,7 +142,7 @@ let module_type_of_module mp mb =
{ mb with
mod_expr = ();
mod_type_alg = None;
- mod_retroknowledge = [] }
+ mod_retroknowledge = ModTypeRK }
in
match mp with
| Some mp -> strengthen {mtb with mod_mp = mp} mp
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 68a467bea..98a9c8250 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -393,7 +393,7 @@ and check_modtypes env mtb1 mtb2 subst1 subst2 equiv =
mod_type = body_t1;
mod_type_alg = None;
mod_constraints = mtb1.mod_constraints;
- mod_retroknowledge = [];
+ mod_retroknowledge = ModBodyRK [];
mod_delta = mtb1.mod_delta} env
in
check_structure env body_t1 body_t2 equiv
diff --git a/checker/values.ml b/checker/values.ml
index f1edabcfb..afde84854 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
with a copy we maintain here:
-MD5 6bfeaec4872c9636faed4967db1502a0 checker/cic.mli
+MD5 62a4037e9e584d508909d631c5e8a759 checker/cic.mli
*)
@@ -318,7 +318,7 @@ and v_module =
[|v_mp;v_impl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|])
and v_modtype =
Tuple ("module_type_body",
- [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|])
+ [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_context_set;v_resolver;v_unit|])
(** kernel/safe_typing *)
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 1b32d343e..e17fb1c38 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -259,7 +259,7 @@ and 'a generic_module_body =
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 }
+ mod_retroknowledge : 'a module_retroknowledge }
(** For a module, there are five possible situations:
- [Declare Module M : T] then [mod_expr = Abstract; mod_type_alg = Some T]
@@ -278,6 +278,11 @@ and module_body = module_implementation generic_module_body
and module_type_body = unit generic_module_body
+and _ module_retroknowledge =
+| ModBodyRK :
+ Retroknowledge.action list -> module_implementation module_retroknowledge
+| ModTypeRK : unit module_retroknowledge
+
(** Extra invariants :
- No [MEwith] inside a [mod_expr] implementation : the 'with' syntax
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index eead5b70d..d2b41aae9 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -283,9 +283,11 @@ let mk_mod mp e ty cst reso =
mod_type_alg = None;
mod_constraints = cst;
mod_delta = reso;
- mod_retroknowledge = [] }
+ mod_retroknowledge = ModBodyRK []; }
-let mk_modtype mp ty cst reso = mk_mod mp () ty cst reso
+let mk_modtype mp ty cst reso =
+ let mb = mk_mod mp Abstract ty cst reso in
+ { mb with mod_expr = (); mod_retroknowledge = ModTypeRK }
let rec translate_mse_funct env mpo inl mse = function
|[] ->
@@ -321,6 +323,7 @@ let finalize_module env mp (sign,alg,reso,cst) restype = match restype with
{ res_mtb with
mod_mp = mp;
mod_expr = impl;
+ mod_retroknowledge = ModBodyRK [];
(** cst from module body typing,
cst' from subtyping,
constraints from module type. *)
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 925d042b1..76915e917 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -143,10 +143,12 @@ let rec functor_iter fty f0 = function
(** {6 Misc operations } *)
let module_type_of_module mb =
- { mb with mod_expr = (); mod_type_alg = None }
+ { mb with mod_expr = (); mod_type_alg = None;
+ mod_retroknowledge = ModTypeRK; }
let module_body_of_type mp mtb =
- { mtb with mod_expr = Abstract; mod_mp = mp }
+ { mtb with mod_expr = Abstract; mod_mp = mp;
+ mod_retroknowledge = ModBodyRK []; }
let check_modpath_equiv env mp1 mp2 =
if ModPath.equal mp1 mp2 then ()
@@ -270,7 +272,7 @@ let add_retroknowledge mp =
CErrors.anomaly ~label:"Modops.add_retroknowledge"
(Pp.str "had to import an unsupported kind of term.")
in
- fun lclrk env ->
+ fun (ModBodyRK lclrk) env ->
(* The order of the declaration matters, for instance (and it's at the
time this comment is being written, the only relevent instance) the
int31 type registration absolutely needs int31 bits to be registered.
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index aa26405f7..ad622b07d 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -677,7 +677,7 @@ let build_module_body params restype senv =
(struc,None,senv.modresolver,senv.univ) restype'
in
let mb' = functorize_module params mb in
- { mb' with mod_retroknowledge = senv.local_retroknowledge }
+ { mb' with mod_retroknowledge = ModBodyRK senv.local_retroknowledge }
(** Returning back to the old pre-interactive-module environment,
with one extra component and some updated fields
@@ -737,7 +737,7 @@ let build_mtb mp sign cst delta =
mod_type_alg = None;
mod_constraints = cst;
mod_delta = delta;
- mod_retroknowledge = [] }
+ mod_retroknowledge = ModTypeRK }
let end_modtype l senv =
let mp = senv.modpath in
@@ -853,7 +853,7 @@ let export ?except senv dir =
mod_type_alg = None;
mod_constraints = senv.univ;
mod_delta = senv.modresolver;
- mod_retroknowledge = senv.local_retroknowledge
+ mod_retroknowledge = ModBodyRK senv.local_retroknowledge
}
in
let ast, symbols =
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index b311165f1..b564b2a8c 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -416,7 +416,7 @@ and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv =
mod_type = subst_signature subst1 body_t1;
mod_type_alg = None;
mod_constraints = mtb1.mod_constraints;
- mod_retroknowledge = [];
+ mod_retroknowledge = ModBodyRK [];
mod_delta = mtb1.mod_delta} env
in
check_structure cst env body_t1 body_t2 equiv subst1 subst2
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 09:34:52 +0000