diff options
| author | Hugo Herbelin | 2017-08-21 18:29:07 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-08-21 18:29:07 +0200 |
| commit | 9dea4814ae928192e23764c09473501e2ecc9937 (patch) | |
| tree | 8fef19360dd8ca299d31369534a729b4925f7a4c /test-suite/failure | |
| parent | 325890a83a2b073d9654b5615c585cd65a376fbd (diff) | |
Ensuring all .v files end with a newline to make "sed -i" work better on them.
Diffstat (limited to 'test-suite/failure')
| -rw-r--r-- | test-suite/failure/circular_subtyping.v | 2 | ||||
| -rw-r--r-- | test-suite/failure/cofixpoint.v | 2 | ||||
| -rw-r--r-- | test-suite/failure/guard-cofix.v | 2 | ||||
| -rw-r--r-- | test-suite/failure/sortelim.v | 2 |
4 files changed, 4 insertions, 4 deletions
diff --git a/test-suite/failure/circular_subtyping.v b/test-suite/failure/circular_subtyping.v index ceccd4607d..9eb7e3bc20 100644 --- a/test-suite/failure/circular_subtyping.v +++ b/test-suite/failure/circular_subtyping.v @@ -7,4 +7,4 @@ Module NN <: T. Module M:=N. End NN. Fail Module P <: T with Module M:=NN := NN. Module F (X:S) (Y:T with Module M:=X). End F. -Fail Module G := F N N.
\ No newline at end of file +Fail Module G := F N N. diff --git a/test-suite/failure/cofixpoint.v b/test-suite/failure/cofixpoint.v index cb39893f47..d193dc484f 100644 --- a/test-suite/failure/cofixpoint.v +++ b/test-suite/failure/cofixpoint.v @@ -12,4 +12,4 @@ Fail CoFixpoint loop : CoFalse := (cofix f := I with g := loop for g). Fail CoFixpoint loop : CoFalse := - (cofix f := loop with g := I for f).
\ No newline at end of file + (cofix f := loop with g := I for f). diff --git a/test-suite/failure/guard-cofix.v b/test-suite/failure/guard-cofix.v index eda4a18673..3ae8770546 100644 --- a/test-suite/failure/guard-cofix.v +++ b/test-suite/failure/guard-cofix.v @@ -40,4 +40,4 @@ Fail CoFixpoint loop' : CoFalse := Omega match eq_sym H in _ = T return T with eq_refl => loop' end end. -Fail Definition ff' : False := match loop' with CF _ t => t end.
\ No newline at end of file +Fail Definition ff' : False := match loop' with CF _ t => t end. diff --git a/test-suite/failure/sortelim.v b/test-suite/failure/sortelim.v index 2b3cf10660..3d2eef6a98 100644 --- a/test-suite/failure/sortelim.v +++ b/test-suite/failure/sortelim.v @@ -146,4 +146,4 @@ Qed. Print Assumptions pandora. -*)
\ No newline at end of file +*) |
