diff options
| author | Pierre-Marie Pédrot | 2020-09-28 11:14:23 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-30 13:20:27 +0200 |
| commit | e3a1cf35313bbc4eaca2a43f5fc95ca306bc45fa (patch) | |
| tree | 288992d95abc5eadcdaa22867ebf0fd944e07a72 /test-suite/output | |
| parent | 2c802aaf74c83274ae922c59081c01bfc267d31b (diff) | |
Remove the forward class hint feature.
It was not documented, not properly tested and thus likely buggy. Judging
from the code alone I spotted already one potential bug. Further more it was
prominently making use of the infamous "arbitrary term as hint" feature.
Since the only user in our CI seems to be a math-classes file that introduced
the feature under a claim of "cleanup", I believe we can safely remove it
without anyone noticing.
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/UnivBinders.out | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 163ed15606..d8d3f696b7 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -67,9 +67,9 @@ mono The command has indeed failed with message: Universe u already exists. bobmorane = -let tt := Type@{UnivBinders.33} in -let ff := Type@{UnivBinders.35} in tt -> ff - : Type@{max(UnivBinders.32,UnivBinders.34)} +let tt := Type@{UnivBinders.32} in +let ff := Type@{UnivBinders.34} in tt -> ff + : Type@{max(UnivBinders.31,UnivBinders.33)} The command has indeed failed with message: Universe u already bound. foo@{E M N} = |