diff options
| author | Pierre-Marie Pédrot | 2020-02-29 13:26:08 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-29 13:42:42 +0100 |
| commit | 54562510ed05bacdf7c9c2a41bb104a68aeaa1c0 (patch) | |
| tree | 50e30af7ef146dde65673bc1972ddf57421a1129 /test-suite | |
| parent | 5c7d89641085e125471db089239e73a064073024 (diff) | |
Be robust in calculating visible ids for non-registered constants.
The previous code was only doing that when either in debug or toplevel mode.
Unfortunately, when dealing with open modules the constants might not have
been registered yet, leading to printing failure. I do not see a reason
why this code should fail when used with globals without a user facing name
when the only goal is to compute a set of identifiers that might clash. Thus,
the above failsafe behaviour is now systematic.
Fixes #8206: Module signature error sometimes prints ??.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/bug_8206.out | 5 | ||||
| -rw-r--r-- | test-suite/output/bug_8206.v | 11 |
2 files changed, 16 insertions, 0 deletions
diff --git a/test-suite/output/bug_8206.out b/test-suite/output/bug_8206.out new file mode 100644 index 0000000000..6015fe32f9 --- /dev/null +++ b/test-suite/output/bug_8206.out @@ -0,0 +1,5 @@ +File "stdin", line 11, characters 0-23: +Error: Signature components for label homework do not match: expected type +"forall a b : nat, bug_8206.M.add a b = bug_8206.M.add b a" but found type +"nat -> forall b : nat, bug_8206.M.add 0 b = bug_8206.M.add b 0". + diff --git a/test-suite/output/bug_8206.v b/test-suite/output/bug_8206.v new file mode 100644 index 0000000000..8d4e73dfac --- /dev/null +++ b/test-suite/output/bug_8206.v @@ -0,0 +1,11 @@ +Module Type Sig. + Parameter add: nat -> nat -> nat. + Axiom homework: forall (a b: nat), add a b = add b a. +End Sig. + +Module Impl. + Definition add(a b: nat) := plus a b. + Axiom homework: forall (a b: nat), add 0 b = add b 0. +End Impl. + +Module M : Sig := Impl. |