diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2016-10-06 19:34:28 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2016-10-06 19:34:28 +0200 |
| commit | fd39a2e844f93b314c2f0b78510f0573cfa1bef3 (patch) | |
| tree | d31080bea8310cdd91d5f13fb74c666d53dfdd86 /toplevel/cerrors.ml | |
| parent | 0a6f0c161756a1878dd81e438df86f08631d8399 (diff) | |
Revert "Make the pretty printer resilient to incomplete nametab (progress on #4363)."
This reverts commit 11ccb7333c2a82d59736027838acaea2237e2402.
This fixes bug #4874. We fallback to the original error message of v8.4.
The fallback printer introduced in this commit only gave unqualified names,
which is what this bug reports.
Diffstat (limited to 'toplevel/cerrors.ml')
0 files changed, 0 insertions, 0 deletions