diff options
| author | Hugo Herbelin | 2020-06-17 17:47:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-07-08 13:40:42 +0200 |
| commit | c68e580377c49435f50f08544c6e9c135f1783a6 (patch) | |
| tree | 75ea77a66b94f99b083d3372c15a3135a0e664eb | |
| parent | 0970c104868e62d580cce290790fe2a910f2c4c0 (diff) | |
Adding test for #12525 (Search of lemmas in Include failing when in Module).
| -rw-r--r-- | test-suite/output/Search.out | 3 | ||||
| -rw-r--r-- | test-suite/output/Search.v | 23 |
2 files changed, 26 insertions, 0 deletions
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. |