diff options
| author | Pierre Letouzey | 2017-07-05 11:34:39 +0200 |
|---|---|---|
| committer | Pierre Letouzey | 2017-07-20 20:31:18 +0200 |
| commit | d8b78fff7fefd606dae5038b69f220b4f3dd706b (patch) | |
| tree | d59cca2422e30ead7d5e13fc67859a1352261f54 /API/API.mli | |
| parent | 4d858df22bb30d2efbef39a177c28c15c600c885 (diff) | |
Extraction: fix bugs 5177 and 5240 (and also indirectly bug 4720)
Avoid Anomaly (or Assert False) when a module signature contains
an applied functor followed by a "with Definition" or "with Module"
Also fix the dependency computation in presence of a "with Definition"
Concerning 4720, the code extracted out of this bug report was suboptimal
in Coq 8.4 (it was compilable, but could have probably been tweaked into a
real issue producing faulty code).
But the example of 4720 (and some variants of it) was broken since 8.5,
for the same reasons as 5177 and 5240. And the good news is that after
these repairs, the example of bug 4720 is now extracted to correct code
(the "with" is preserved).
Diffstat (limited to 'API/API.mli')
| -rw-r--r-- | API/API.mli | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/API/API.mli b/API/API.mli index b1a746e028..c52c305853 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1299,12 +1299,19 @@ sig | DefinitionEntry of 'a definition_entry | ParameterEntry of parameter_entry | ProjectionEntry of projection_entry + type module_struct_entry = Declarations.module_alg_expr + type module_params_entry = + (Names.MBId.t * module_struct_entry) list + type module_type_entry = module_params_entry * module_struct_entry end module Mod_typing : sig type 'alg translation = Declarations.module_signature * 'alg * Mod_subst.delta_resolver * Univ.ContextSet.t + val translate_modtype : + Environ.env -> Names.ModPath.t -> Entries.inline -> + Entries.module_type_entry -> Declarations.module_type_body val translate_mse : Environ.env -> Names.ModPath.t option -> Entries.inline -> Declarations.module_alg_expr -> Declarations.module_alg_expr translation |