diff options
| author | Matthieu Sozeau | 2014-05-16 19:25:16 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-16 19:48:22 +0200 |
| commit | d483b7171dafadbe01520bbb6d0c75aa0d6099a7 (patch) | |
| tree | 83141262795fdce2c4c24b62e89e913cb1952349 /test-suite/bugs | |
| parent | e321cfd21e28161923b84d943cb15c6d775b0d9e (diff) | |
Fix unification of non-unfoldable primitive projections in evarconv.
Diffstat (limited to 'test-suite/bugs')
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_122.v (renamed from test-suite/bugs/opened/HoTT_coq_122.v) | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/opened/HoTT_coq_122.v b/test-suite/bugs/closed/HoTT_coq_122.v index 7e474d0a12..1ba8e5c345 100644 --- a/test-suite/bugs/opened/HoTT_coq_122.v +++ b/test-suite/bugs/closed/HoTT_coq_122.v @@ -22,4 +22,4 @@ Record PreCategory := left_identity : forall a b (f : morphism a b), identity b o f = f }. -Fail Timeout 1 Hint Rewrite @left_identity. (* stack overflow *) +Hint Rewrite @left_identity. (* stack overflow *) |