From 0970c104868e62d580cce290790fe2a910f2c4c0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 17 Jun 2020 17:30:20 +0200 Subject: Preserve delta-resolver at Module and Module Type starting. The default value of the delta-resolver for name aliasing was reinitialized at Module and Module Type starting time. The existing resolver was saved but the saved value was not used in Safe_typing.constant_of_delta_kn_senv and Safe_typing.mind_of_delta_kn_senv. A possible fix could have been to take the saved resolver into account in Safe_typing.constant_of_delta_kn_senv and Safe_typing.mind_of_delta_kn_senv. We just try instead not to reinitialize it. This incidentally fixes #12525 (Search unable to see through an "Include" when in an ongoing "Module"). --- kernel/safe_typing.ml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 93337fca5d..8b85072d6d 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1023,6 +1023,8 @@ let start_module l senv = mp, { empty_environment with env = senv.env; + modresolver = senv.modresolver; + paramresolver = senv.paramresolver; modpath = mp; modvariant = STRUCT ([],senv); required = senv.required } @@ -1034,6 +1036,8 @@ let start_modtype l senv = mp, { empty_environment with env = senv.env; + modresolver = senv.modresolver; + paramresolver = senv.paramresolver; modpath = mp; modvariant = SIG ([], senv); required = senv.required } -- cgit v1.2.3 From c68e580377c49435f50f08544c6e9c135f1783a6 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 17 Jun 2020 17:47:03 +0200 Subject: Adding test for #12525 (Search of lemmas in Include failing when in Module). --- test-suite/output/Search.out | 3 +++ test-suite/output/Search.v | 23 +++++++++++++++++++++++ 2 files changed, 26 insertions(+) diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index 317e9c3757..09feca71e7 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -455,3 +455,6 @@ PreOrder_Reflexive: reflexive_eq_dom_reflexive: forall {A B : Type} {R' : Relation_Definitions.relation B}, Reflexive R' -> Reflexive (eq ==> R')%signature +B.b: B.a +A.b: A.a +F.L: F.P 0 diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v index 4ec7a760b9..a5ac2cb511 100644 --- a/test-suite/output/Search.v +++ b/test-suite/output/Search.v @@ -66,3 +66,26 @@ Reset Initial. Require Import Morphisms. Search is:Instance [ Reflexive | Symmetric ]. + +Module Bug12525. + (* This was revealing a kernel bug with delta-resolution *) + Module A. Axiom a:Prop. Axiom b:a. End A. + Module B. Include A. End B. + Module M. + Search B.a. + End M. +End Bug12525. + +From Coq Require Lia. + +Module Bug12647. + (* Similar to #12525 *) + Module Type Foo. + Axiom P : nat -> Prop. + Axiom L : P 0. + End Foo. + + Module Bar (F : Foo). + Search F.P. + End Bar. +End Bug12647. -- cgit v1.2.3 From 0046a166843495b131fb197788c28de9b4705685 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 17 Jun 2020 18:08:31 +0200 Subject: Adding change log. --- .../12537-master+module-starting-extends-delta-resolver.rst | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100644 doc/changelog/01-kernel/12537-master+module-starting-extends-delta-resolver.rst diff --git a/doc/changelog/01-kernel/12537-master+module-starting-extends-delta-resolver.rst b/doc/changelog/01-kernel/12537-master+module-starting-extends-delta-resolver.rst new file mode 100644 index 0000000000..bec121836c --- /dev/null +++ b/doc/changelog/01-kernel/12537-master+module-starting-extends-delta-resolver.rst @@ -0,0 +1,8 @@ +- **Fixed:** + A loss of definitional equality for declarations obtained through + :cmd:`Include` when entering the scope of a :cmd:`Module` or + :cmd:`Module Type` was causing :cmd:`Search` not to see the included + declarations + (`#12537 `_, fixes `#12525 + `_ and `#12647 + `_, by Hugo Herbelin). -- cgit v1.2.3