diff options
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 7c5dc41679..0b576db6b3 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 10c988fc02..57c1744313 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 99ca6cb39d..e4711a38c0 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 165813084d..5c4b4277b2 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. |
