summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/2734.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/closed/2734.v')
-rw-r--r--test-suite/bugs/closed/2734.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/2734.v b/test-suite/bugs/closed/2734.v
index 826361be..3210214e 100644
--- a/test-suite/bugs/closed/2734.v
+++ b/test-suite/bugs/closed/2734.v
@@ -12,4 +12,4 @@ Inductive control := Go: expr -> control.
Definition program := (Adr.t * (control))%type.
-Fail Definition myprog : program := (Adr.nat2t 0, Go (Adr.nat2t 0) ). \ No newline at end of file
+Fail Definition myprog : program := (Adr.nat2t 0, Go (Adr.nat2t 0) ).