aboutsummaryrefslogtreecommitdiff
path: root/test-suite/typeclasses
diff options
context:
space:
mode:
authorMaxime Dénès2017-09-15 09:54:58 +0200
committerMaxime Dénès2017-09-15 09:54:58 +0200
commite559709f7ac6e997d50d7af2f9e2a230ce2f7daa (patch)
tree650cab1e954d3fa4ed36b17f2822ff915f1af289 /test-suite/typeclasses
parent5bac7458e037879142eb468fc4695b996189a20b (diff)
parent9dea4814ae928192e23764c09473501e2ecc9937 (diff)
Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" work better on them
Diffstat (limited to 'test-suite/typeclasses')
-rw-r--r--test-suite/typeclasses/deftwice.v2
-rw-r--r--test-suite/typeclasses/unification_delta.v2
2 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/typeclasses/deftwice.v b/test-suite/typeclasses/deftwice.v
index 439782c9e5..1394477027 100644
--- a/test-suite/typeclasses/deftwice.v
+++ b/test-suite/typeclasses/deftwice.v
@@ -6,4 +6,4 @@ Instance inhab_C : C Type := Inhab.
Variable full : forall A (X : C A), forall x : A, c x.
-Definition truc {A : Type} : Inhab A := (full _ _ _). \ No newline at end of file
+Definition truc {A : Type} : Inhab A := (full _ _ _).
diff --git a/test-suite/typeclasses/unification_delta.v b/test-suite/typeclasses/unification_delta.v
index 663a837f36..518912433d 100644
--- a/test-suite/typeclasses/unification_delta.v
+++ b/test-suite/typeclasses/unification_delta.v
@@ -43,4 +43,4 @@ Proof.
(* Breaks if too much delta in unification *)
rewrite H.
reflexivity.
-Qed. \ No newline at end of file
+Qed.