diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-09-20 00:06:33 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-09-20 00:14:32 +0200 |
| commit | bfd0ee9503cf04b51b2dd40d4ad2a904b07ac323 (patch) | |
| tree | 3cc2e5b414ab0b5a8aa00b2023982dc40ae00ca7 | |
| parent | 04e9be59051ca60bf61d5142ac14386920876926 (diff) | |
Fix #3948 Anomaly: unknown constant in Print Assumptions
Substitution on bound modules was incorrectly extended without sequential
composition.
| -rw-r--r-- | kernel/mod_subst.ml | 2 | ||||
| -rw-r--r-- | kernel/mod_subst.mli | 5 | ||||
| -rw-r--r-- | toplevel/assumptions.ml | 12 |
3 files changed, 10 insertions, 9 deletions
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index f7ae30e7a..ba14f65d9 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -122,7 +122,7 @@ let add_kn_delta_resolver kn kn' = let add_mp_delta_resolver mp1 mp2 = Deltamap.add_mp mp1 mp2 -(** Extending a [substitution] *) +(** Extending a [substitution] without sequential composition *) let add_mbid mbid mp resolve s = Umap.add_mbi mbid (mp,resolve) s let add_mp mp1 mp2 resolve s = Umap.add_mp mp1 (mp2,resolve) s diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index fc2b0441c..cd9fa7921 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -68,8 +68,9 @@ val empty_subst : substitution val is_empty_subst : substitution -> bool -(** add_* add [arg2/arg1]\{arg3\} to the substitution with no - sequential composition *) +(** add_* add [arg2/arg1]\{arg3\} to the substitution with no sequential + composition. Most often this is not what you want. For sequential + composition, try [join (map_mbid mp delta) subs] **) val add_mbid : MBId.t -> module_path -> delta_resolver -> substitution -> substitution val add_mp : diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml index 4d8ba0f78..a6bd968ef 100644 --- a/toplevel/assumptions.ml +++ b/toplevel/assumptions.ml @@ -55,7 +55,7 @@ let rec fields_of_functor f subs mp0 args = function match args with | [] -> assert false (* we should only encounter applied functors *) | mpa :: args -> - let subs = add_mbid mbid mpa empty_delta_resolver (*TODO*) subs in + let subs = join (map_mbid mbid mpa empty_delta_resolver (*TODO*)) subs in fields_of_functor f subs mp0 args e let rec lookup_module_in_impl mp = @@ -64,11 +64,11 @@ let rec lookup_module_in_impl mp = (* The module we search might not be exported by its englobing module(s). We access the upper layer, and then do a manual search *) match mp with - | MPfile _ | MPbound _ -> - raise Not_found (* should have been found by [lookup_module] *) - | MPdot (mp',lab') -> - let fields = memoize_fields_of_mp mp' in - search_mod_label lab' fields + | MPfile _ -> raise Not_found (* can happen if mp is an open module *) + | MPbound _ -> assert false + | MPdot (mp',lab') -> + let fields = memoize_fields_of_mp mp' in + search_mod_label lab' fields and memoize_fields_of_mp mp = try MPmap.find mp !modcache |