diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-21 18:29:07 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-21 18:29:07 +0200 |
| commit | 9dea4814ae928192e23764c09473501e2ecc9937 (patch) | |
| tree | 8fef19360dd8ca299d31369534a729b4925f7a4c /test-suite/bugs/opened | |
| parent | 325890a83a2b073d9654b5615c585cd65a376fbd (diff) | |
Ensuring all .v files end with a newline to make "sed -i" work better on them.
Diffstat (limited to 'test-suite/bugs/opened')
| -rw-r--r-- | test-suite/bugs/opened/1596.v | 2 | ||||
| -rw-r--r-- | test-suite/bugs/opened/1811.v | 2 | ||||
| -rw-r--r-- | test-suite/bugs/opened/3794.v | 2 | ||||
| -rw-r--r-- | test-suite/bugs/opened/3948.v | 2 |
4 files changed, 4 insertions, 4 deletions
diff --git a/test-suite/bugs/opened/1596.v b/test-suite/bugs/opened/1596.v index 7c5dc4167..0b576db6b 100644 --- a/test-suite/bugs/opened/1596.v +++ b/test-suite/bugs/opened/1596.v @@ -258,4 +258,4 @@ n). apply SynInc;apply H.mem_2;trivial. rewrite H in H0. discriminate. (* !! impossible here !! *) Qed. -End B.
\ No newline at end of file +End B. diff --git a/test-suite/bugs/opened/1811.v b/test-suite/bugs/opened/1811.v index 10c988fc0..57c174431 100644 --- a/test-suite/bugs/opened/1811.v +++ b/test-suite/bugs/opened/1811.v @@ -7,4 +7,4 @@ Goal forall b1 b2, (negb b1 = b2) -> xorb true b1 = b2. Proof. intros b1 b2. Fail rewrite neg2xor. -Abort.
\ No newline at end of file +Abort. diff --git a/test-suite/bugs/opened/3794.v b/test-suite/bugs/opened/3794.v index 99ca6cb39..e4711a38c 100644 --- a/test-suite/bugs/opened/3794.v +++ b/test-suite/bugs/opened/3794.v @@ -4,4 +4,4 @@ Hint Unfold not : core. Goal true<>false. Set Typeclasses Debug. Fail typeclasses eauto with core. -Abort.
\ No newline at end of file +Abort. diff --git a/test-suite/bugs/opened/3948.v b/test-suite/bugs/opened/3948.v index 165813084..5c4b4277b 100644 --- a/test-suite/bugs/opened/3948.v +++ b/test-suite/bugs/opened/3948.v @@ -22,4 +22,4 @@ Module DepMap : Interface. let _ := @Dom.fold in tt. End DepMap. -Print Assumptions DepMap.constant.
\ No newline at end of file +Print Assumptions DepMap.constant. |