diff options
Diffstat (limited to 'test-suite/bugs/closed/3484.v')
| -rw-r--r-- | test-suite/bugs/closed/3484.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/3484.v b/test-suite/bugs/closed/3484.v index dc88a332..a0e15730 100644 --- a/test-suite/bugs/closed/3484.v +++ b/test-suite/bugs/closed/3484.v @@ -28,4 +28,4 @@ T : Type H : sigT T (fun g : T => paths g g) x : T Unable to unify "paths (@projT1 ?24 ?23 ?25) (@projT1 ?24 ?23 ?26)" with - "paths (projT1 H) (projT1 {| projT1 := x; projT2 := idpath |})". *)
\ No newline at end of file + "paths (projT1 H) (projT1 {| projT1 := x; projT2 := idpath |})". *) |