diff options
| author | Hugo Herbelin | 2018-09-05 21:56:06 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-05 22:26:59 +0200 |
| commit | 899f3eb1f65ad2e6a3fababa0213ac63e2501bbe (patch) | |
| tree | 301b3ecc7729b38ef1f2066910ff6ea298db8e6c /test-suite/output | |
| parent | 579f30a53809f9cf73aa3d7c69960b50fc51c7fc (diff) | |
Fixing #8416 (Print Assumptions missing module information from compiled files).
This fixes the fix 1522b989 to #7192.
The remaining Not_found after 1522b989 should have rung a bell that
something was still strange.
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/PrintAssumptions.out | 2 | ||||
| -rw-r--r-- | test-suite/output/PrintAssumptions.v | 10 |
2 files changed, 12 insertions, 0 deletions
diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out index 34f44cd246..3f4d5ef58c 100644 --- a/test-suite/output/PrintAssumptions.out +++ b/test-suite/output/PrintAssumptions.out @@ -20,3 +20,5 @@ Axioms: M.foo : False Closed under the global context Closed under the global context +Closed under the global context +Closed under the global context diff --git a/test-suite/output/PrintAssumptions.v b/test-suite/output/PrintAssumptions.v index ea1ab63786..3d4dfe603d 100644 --- a/test-suite/output/PrintAssumptions.v +++ b/test-suite/output/PrintAssumptions.v @@ -137,3 +137,13 @@ Module F (X : T). End F. End SUBMODULES. + +(* Testing a variant of #7192 across files *) +(* This was missing in the original fix to #7192 *) +Require Import module_bug7192. +Print Assumptions M7192.D.f. + +(* Testing reporting assumptions from modules in files *) +(* A regression introduced in the original fix to #7192 was missing implementations *) +Require Import module_bug8416. +Print Assumptions M8416.f. |