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 | |
| parent | 325890a83a2b073d9654b5615c585cd65a376fbd (diff) | |
Ensuring all .v files end with a newline to make "sed -i" work better on them.
199 files changed, 199 insertions, 199 deletions
diff --git a/plugins/derive/Derive.v b/plugins/derive/Derive.v index 0d5a93b03..d1046ae79 100644 --- a/plugins/derive/Derive.v +++ b/plugins/derive/Derive.v @@ -1 +1 @@ -Declare ML Module "derive_plugin".
\ No newline at end of file +Declare ML Module "derive_plugin". diff --git a/plugins/extraction/ExtrHaskellNatNum.v b/plugins/extraction/ExtrHaskellNatNum.v index fabe9a4c6..09b044461 100644 --- a/plugins/extraction/ExtrHaskellNatNum.v +++ b/plugins/extraction/ExtrHaskellNatNum.v @@ -34,4 +34,4 @@ Extract Constant Init.Nat.sub => "(\n m -> Prelude.max 0 (n Prelude.- m))". Extract Constant Nat.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)". Extract Constant Nat.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)". Extract Constant Init.Nat.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)". -Extract Constant Init.Nat.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)".
\ No newline at end of file +Extract Constant Init.Nat.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)". diff --git a/plugins/extraction/ExtrOcamlIntConv.v b/plugins/extraction/ExtrOcamlIntConv.v index fe6eb7780..ab13d75ad 100644 --- a/plugins/extraction/ExtrOcamlIntConv.v +++ b/plugins/extraction/ExtrOcamlIntConv.v @@ -96,4 +96,4 @@ Extraction "/tmp/test.ml" pos_of_int int_of_pos z_of_int int_of_z n_of_int int_of_n. -*)
\ No newline at end of file +*) diff --git a/plugins/extraction/Extraction.v b/plugins/extraction/Extraction.v index 1374a91ab..b3f9d6556 100644 --- a/plugins/extraction/Extraction.v +++ b/plugins/extraction/Extraction.v @@ -6,4 +6,4 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Declare ML Module "extraction_plugin".
\ No newline at end of file +Declare ML Module "extraction_plugin". diff --git a/plugins/romega/ROmega.v b/plugins/romega/ROmega.v index 3ddb6bed1..657aae90e 100644 --- a/plugins/romega/ROmega.v +++ b/plugins/romega/ROmega.v @@ -11,4 +11,4 @@ Require Export Setoid. Require Export PreOmega. Require Export ZArith_base. Require Import OmegaPlugin. -Declare ML Module "romega_plugin".
\ No newline at end of file +Declare ML Module "romega_plugin". diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v index 329fa0ee8..36d1e7c54 100644 --- a/plugins/setoid_ring/Ring_tac.v +++ b/plugins/setoid_ring/Ring_tac.v @@ -460,4 +460,4 @@ Tactic Notation "ring_simplify" "["constr_list(lH)"]" constr_list(rl) "in" hyp(H intro H'; move H' after H; clear H;rename H' into H; - unfold g;clear g.
\ No newline at end of file + unfold g;clear g. diff --git a/test-suite/bugs/4623.v b/test-suite/bugs/4623.v index 405d09809..7ecfd98b6 100644 --- a/test-suite/bugs/4623.v +++ b/test-suite/bugs/4623.v @@ -2,4 +2,4 @@ Goal Type -> Type. set (T := Type). clearbody T. refine (@id _). -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/4624.v b/test-suite/bugs/4624.v index a737afcda..f5ce981cd 100644 --- a/test-suite/bugs/4624.v +++ b/test-suite/bugs/4624.v @@ -4,4 +4,4 @@ Canonical Structure fooA (T : Type) := mkfoo (T -> T). Definition id (t : foo) (x : type t) := x. -Definition bar := id _ ((fun x : nat => x) : _).
\ No newline at end of file +Definition bar := id _ ((fun x : nat => x) : _). diff --git a/test-suite/bugs/closed/1425.v b/test-suite/bugs/closed/1425.v index 6be30174a..775d278e7 100644 --- a/test-suite/bugs/closed/1425.v +++ b/test-suite/bugs/closed/1425.v @@ -16,4 +16,4 @@ Goal forall n : nat, recursion nat 0 (fun _ _ => 1) (S n) = 1. intro n. setoid_rewrite recursion_S. reflexivity. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/1738.v b/test-suite/bugs/closed/1738.v index c2926a2b2..ef52c876c 100644 --- a/test-suite/bugs/closed/1738.v +++ b/test-suite/bugs/closed/1738.v @@ -27,4 +27,4 @@ Module Test (Import M:FSetInterface.S). rewrite H in H0. assumption. Qed. -End Test.
\ No newline at end of file +End Test. diff --git a/test-suite/bugs/closed/1900.v b/test-suite/bugs/closed/1900.v index cf03efda4..6eea5db08 100644 --- a/test-suite/bugs/closed/1900.v +++ b/test-suite/bugs/closed/1900.v @@ -5,4 +5,4 @@ Definition eq_A := @eq A. Goal forall x, eq_A x x. intros. reflexivity. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/1901.v b/test-suite/bugs/closed/1901.v index 7d86adbfb..98e017f9d 100644 --- a/test-suite/bugs/closed/1901.v +++ b/test-suite/bugs/closed/1901.v @@ -8,4 +8,4 @@ Record Poset{A:Type}(Le : relation A) : Type := Le_antisym : forall x y : A, Le x y -> Le y x -> x = y }. Definition nat_Poset : Poset Peano.le. -Admitted.
\ No newline at end of file +Admitted. diff --git a/test-suite/bugs/closed/1905.v b/test-suite/bugs/closed/1905.v index 8c81d7510..3b8a3d2f6 100644 --- a/test-suite/bugs/closed/1905.v +++ b/test-suite/bugs/closed/1905.v @@ -10,4 +10,4 @@ Goal forall a s, Proof. intros a s Ia. rewrite InE in Ia. -Admitted.
\ No newline at end of file +Admitted. diff --git a/test-suite/bugs/closed/1915.v b/test-suite/bugs/closed/1915.v index 7e62437d7..2b0aed8c7 100644 --- a/test-suite/bugs/closed/1915.v +++ b/test-suite/bugs/closed/1915.v @@ -3,4 +3,4 @@ Require Import Setoid. Fail Goal forall x, impl True (x = 0) -> x = 0 -> False. (*intros x H E. -rewrite H in E.*)
\ No newline at end of file +rewrite H in E.*) diff --git a/test-suite/bugs/closed/1939.v b/test-suite/bugs/closed/1939.v index 5e61529b4..7b430ace5 100644 --- a/test-suite/bugs/closed/1939.v +++ b/test-suite/bugs/closed/1939.v @@ -16,4 +16,4 @@ Require Import Setoid Program.Basics. intros x y H1 H2. rewrite H1. auto. - Qed.
\ No newline at end of file + Qed. diff --git a/test-suite/bugs/closed/1962.v b/test-suite/bugs/closed/1962.v index a6b0fee58..37b0dde06 100644 --- a/test-suite/bugs/closed/1962.v +++ b/test-suite/bugs/closed/1962.v @@ -52,4 +52,4 @@ unfold triple, couple. Time fsetdec. Qed. -End BuildFSets.
\ No newline at end of file +End BuildFSets. diff --git a/test-suite/bugs/closed/2027.v b/test-suite/bugs/closed/2027.v index fb53c6ef4..ebc2bc070 100644 --- a/test-suite/bugs/closed/2027.v +++ b/test-suite/bugs/closed/2027.v @@ -8,4 +8,4 @@ Goal forall A (p : T A), P p. Proof. intros. rewrite <- f_id. -Admitted.
\ No newline at end of file +Admitted. diff --git a/test-suite/bugs/closed/2136.v b/test-suite/bugs/closed/2136.v index d2b926f37..2fcfbe40d 100644 --- a/test-suite/bugs/closed/2136.v +++ b/test-suite/bugs/closed/2136.v @@ -58,4 +58,4 @@ fsetdec. (* Error: Tactic failure: because the goal is beyond the scope of this tactic. *) -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/2137.v b/test-suite/bugs/closed/2137.v index 6c2023ab7..b1f54b176 100644 --- a/test-suite/bugs/closed/2137.v +++ b/test-suite/bugs/closed/2137.v @@ -49,4 +49,4 @@ fsetdec. (* Error: Tactic failure: because the goal is beyond the scope of this tactic. *) -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/2141.v b/test-suite/bugs/closed/2141.v index c556ff0b2..22e33c8e8 100644 --- a/test-suite/bugs/closed/2141.v +++ b/test-suite/bugs/closed/2141.v @@ -13,4 +13,4 @@ Module NatSet' := FSetHide NatSet. Recursive Extraction NatSet'.fold. Extraction TestCompile NatSet'.fold. -(* Extraction "test2141.ml" NatSet'.fold. *)
\ No newline at end of file +(* Extraction "test2141.ml" NatSet'.fold. *) diff --git a/test-suite/bugs/closed/2281.v b/test-suite/bugs/closed/2281.v index 40948d905..8f549b920 100644 --- a/test-suite/bugs/closed/2281.v +++ b/test-suite/bugs/closed/2281.v @@ -47,4 +47,4 @@ intros. fsetdec. (* Error: Tactic failure: because the goal is beyond the scope of this tactic. *) -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/2310.v b/test-suite/bugs/closed/2310.v index 7fae32871..14a3e5a7b 100644 --- a/test-suite/bugs/closed/2310.v +++ b/test-suite/bugs/closed/2310.v @@ -18,4 +18,4 @@ Definition replace a (y:Nest (prod a a)) : a = a -> Nest a. Unset Solve Unification Constraints. (* Keep the unification constraint around *) refine (Cons (cast H _ y)). intros. - refine (Nest (prod X X)). Qed.
\ No newline at end of file + refine (Nest (prod X X)). Qed. diff --git a/test-suite/bugs/closed/2319.v b/test-suite/bugs/closed/2319.v index e06fb9759..73d95e91a 100644 --- a/test-suite/bugs/closed/2319.v +++ b/test-suite/bugs/closed/2319.v @@ -10,4 +10,4 @@ Section S. with t : A unit := mkA unit (mkA unit t). Timeout 5 Eval vm_compute in s. -End S.
\ No newline at end of file +End S. diff --git a/test-suite/bugs/closed/2464.v b/test-suite/bugs/closed/2464.v index af7085872..b9db30359 100644 --- a/test-suite/bugs/closed/2464.v +++ b/test-suite/bugs/closed/2464.v @@ -36,4 +36,4 @@ Lemma foo : forall (pu_type : Type) NameSetMod.Equal ns2 (NameSetMod.add (pu_nameOf p) ns). Proof. NameSetDec.fsetdec. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/2473.v b/test-suite/bugs/closed/2473.v index fb676c7e4..0e7c0c25f 100644 --- a/test-suite/bugs/closed/2473.v +++ b/test-suite/bugs/closed/2473.v @@ -37,4 +37,4 @@ Section S3. rewrite <- H. (* ok *) admit. Qed. -End S3.
\ No newline at end of file +End S3. diff --git a/test-suite/bugs/closed/2584.v b/test-suite/bugs/closed/2584.v index a5f4ae64a..ef2e4e355 100644 --- a/test-suite/bugs/closed/2584.v +++ b/test-suite/bugs/closed/2584.v @@ -86,4 +86,4 @@ should be "Prop" or "Set". Elimination of an inductive object of sort Set is not allowed on a predicate in sort Type because strong elimination on non-small inductive types leads to paradoxes. -*)
\ No newline at end of file +*) diff --git a/test-suite/bugs/closed/2586.v b/test-suite/bugs/closed/2586.v index 7e02e7f11..e57bcc25b 100644 --- a/test-suite/bugs/closed/2586.v +++ b/test-suite/bugs/closed/2586.v @@ -3,4 +3,4 @@ Require Import Setoid SetoidClass Program. Goal forall `(Setoid nat) x y, x == y -> S x == S y. intros. Fail clsubst H0. - Abort.
\ No newline at end of file + Abort. diff --git a/test-suite/bugs/closed/2602.v b/test-suite/bugs/closed/2602.v index f07447886..29c8ac16b 100644 --- a/test-suite/bugs/closed/2602.v +++ b/test-suite/bugs/closed/2602.v @@ -5,4 +5,4 @@ match goal with match goal with | |- S a > 0 => idtac end -end.
\ No newline at end of file +end. diff --git a/test-suite/bugs/closed/2615.v b/test-suite/bugs/closed/2615.v index 38c1cfc84..26c0f334d 100644 --- a/test-suite/bugs/closed/2615.v +++ b/test-suite/bugs/closed/2615.v @@ -14,4 +14,4 @@ refine (fun p => match p with _ => _ end). Undo. refine (fun p => match p with foo_intro _ _ => _ end). admit. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/2668.v b/test-suite/bugs/closed/2668.v index 74c8fa347..d5bbfd3f0 100644 --- a/test-suite/bugs/closed/2668.v +++ b/test-suite/bugs/closed/2668.v @@ -3,4 +3,4 @@ Require Import MSetProperties. Module Pos := MSetPositive.PositiveSet. Module PPPP := MSetProperties.WPropertiesOn(Pos). -Print Module PPPP.
\ No newline at end of file +Print Module PPPP. diff --git a/test-suite/bugs/closed/2734.v b/test-suite/bugs/closed/2734.v index 826361be2..3210214ea 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) ). diff --git a/test-suite/bugs/closed/2750.v b/test-suite/bugs/closed/2750.v index fc580f101..9d65e51f6 100644 --- a/test-suite/bugs/closed/2750.v +++ b/test-suite/bugs/closed/2750.v @@ -20,4 +20,4 @@ Module Test_ModWithRecord (M : ModWithRecord). {| M.A := 0 ; M.B := 2 |}. -End Test_ModWithRecord.
\ No newline at end of file +End Test_ModWithRecord. diff --git a/test-suite/bugs/closed/2837.v b/test-suite/bugs/closed/2837.v index 5d9844639..52a56c2cf 100644 --- a/test-suite/bugs/closed/2837.v +++ b/test-suite/bugs/closed/2837.v @@ -12,4 +12,4 @@ Fail rewrite test. Fail (intros; rewrite test). (* III) a working variant: *) -intros; rewrite (test n m).
\ No newline at end of file +intros; rewrite (test n m). diff --git a/test-suite/bugs/closed/2848.v b/test-suite/bugs/closed/2848.v index 828e3b8c1..e23463033 100644 --- a/test-suite/bugs/closed/2848.v +++ b/test-suite/bugs/closed/2848.v @@ -7,4 +7,4 @@ Add Parametric Relation : _ equiv' reflexivity proved by (Equivalence.equiv_reflexive cheat) transitivity proved by (Equivalence.equiv_transitive cheat) as apply_equiv'_rel. -Check apply_equiv'_rel : PreOrder equiv'.
\ No newline at end of file +Check apply_equiv'_rel : PreOrder equiv'. diff --git a/test-suite/bugs/closed/2955.v b/test-suite/bugs/closed/2955.v index 45e24b5f5..11fd7bada 100644 --- a/test-suite/bugs/closed/2955.v +++ b/test-suite/bugs/closed/2955.v @@ -49,4 +49,4 @@ Module E. assumption. Qed. -End E.
\ No newline at end of file +End E. diff --git a/test-suite/bugs/closed/2983.v b/test-suite/bugs/closed/2983.v index 15598352b..ad7635094 100644 --- a/test-suite/bugs/closed/2983.v +++ b/test-suite/bugs/closed/2983.v @@ -5,4 +5,4 @@ End ModB. Module Foo(A : ModA)(B : ModB A). End Foo. -Print Module Foo.
\ No newline at end of file +Print Module Foo. diff --git a/test-suite/bugs/closed/2995.v b/test-suite/bugs/closed/2995.v index ba3acd088..b6c5b6df4 100644 --- a/test-suite/bugs/closed/2995.v +++ b/test-suite/bugs/closed/2995.v @@ -6,4 +6,4 @@ Module Implementation <: Interface. Definition t := bool. Definition error: t := false. Fail End Implementation. -(* A UserError here is expected, not an uncaught Not_found *)
\ No newline at end of file +(* A UserError here is expected, not an uncaught Not_found *) diff --git a/test-suite/bugs/closed/3008.v b/test-suite/bugs/closed/3008.v index 3f3a979a3..1979eda82 100644 --- a/test-suite/bugs/closed/3008.v +++ b/test-suite/bugs/closed/3008.v @@ -26,4 +26,4 @@ Fail Module Toto (* NB : the Inductive above and the A=A weren't in the initial test, they are here only to force an access to the environment - (cf [Printer.qualid_of_global]) and check that this env is ok. *)
\ No newline at end of file + (cf [Printer.qualid_of_global]) and check that this env is ok. *) diff --git a/test-suite/bugs/closed/3319.v b/test-suite/bugs/closed/3319.v index 3b37e39e5..fbf5d86dc 100644 --- a/test-suite/bugs/closed/3319.v +++ b/test-suite/bugs/closed/3319.v @@ -23,4 +23,4 @@ Section precategory. = morphism' xa yb. Proof. admit. - Defined.
\ No newline at end of file + Defined. diff --git a/test-suite/bugs/closed/3331.v b/test-suite/bugs/closed/3331.v index 9cd44bd0c..b7dbb290e 100644 --- a/test-suite/bugs/closed/3331.v +++ b/test-suite/bugs/closed/3331.v @@ -28,4 +28,4 @@ Section groupoid_category. clear H' foo. Set Typeclasses Debug. pose (_ : Contr (idpath = idpath :> (@paths (@paths X d d) idpath idpath))). -Abort.
\ No newline at end of file +Abort. diff --git a/test-suite/bugs/closed/3352.v b/test-suite/bugs/closed/3352.v index 555accfd5..bf2f7a9d1 100644 --- a/test-suite/bugs/closed/3352.v +++ b/test-suite/bugs/closed/3352.v @@ -32,4 +32,4 @@ simpl. Set Printing Universes. exact hprop_Empty. Defined. -End B.
\ No newline at end of file +End B. diff --git a/test-suite/bugs/closed/3387.v b/test-suite/bugs/closed/3387.v index cb435e786..1d9e78337 100644 --- a/test-suite/bugs/closed/3387.v +++ b/test-suite/bugs/closed/3387.v @@ -19,4 +19,4 @@ Proof. first [ unify x y | fail 2 "no unify" ]; change x with y at -1. (* Error: Not convertible. *) reflexivity. -Defined.
\ No newline at end of file +Defined. diff --git a/test-suite/bugs/closed/3392.v b/test-suite/bugs/closed/3392.v index 3a5986954..a03db7754 100644 --- a/test-suite/bugs/closed/3392.v +++ b/test-suite/bugs/closed/3392.v @@ -37,4 +37,4 @@ Proof. rewrite eissect; apply apD ). -Defined.
\ No newline at end of file +Defined. diff --git a/test-suite/bugs/closed/3402.v b/test-suite/bugs/closed/3402.v index ed47ec825..b4705780d 100644 --- a/test-suite/bugs/closed/3402.v +++ b/test-suite/bugs/closed/3402.v @@ -4,4 +4,4 @@ Goal forall A B (p : prod A B), p = let (x, y) := p in pair A B x y. Proof. intros A B p. exact eq_refl. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/3428.v b/test-suite/bugs/closed/3428.v index 3eb75e43a..16ace90af 100644 --- a/test-suite/bugs/closed/3428.v +++ b/test-suite/bugs/closed/3428.v @@ -32,4 +32,4 @@ z' : prod A B p : @paths A (foo.fst ?11 ?14 z) (foo.fst ?26 ?29 z') q : @paths ?54 (foo.snd ?42 ?45 z) (foo.snd ?57 ?60 z') The term "p" has type "@paths A (foo.fst ?11 ?14 z) (foo.fst ?26 ?29 z')" -while it is expected to have type "@paths A (foo.fst z) (foo.fst z')". *)
\ No newline at end of file +while it is expected to have type "@paths A (foo.fst z) (foo.fst z')". *) diff --git a/test-suite/bugs/closed/3439.v b/test-suite/bugs/closed/3439.v index 1ea24bf1b..e8c2d8b8c 100644 --- a/test-suite/bugs/closed/3439.v +++ b/test-suite/bugs/closed/3439.v @@ -41,4 +41,4 @@ Module prim. Undo. solve [ typeclasses eauto ]. (* Error: No applicable tactic. *) Defined. -End prim.
\ No newline at end of file +End prim. diff --git a/test-suite/bugs/closed/3441.v b/test-suite/bugs/closed/3441.v index 50d297807..ddfb33944 100644 --- a/test-suite/bugs/closed/3441.v +++ b/test-suite/bugs/closed/3441.v @@ -20,4 +20,4 @@ Timeout 1 let H := fresh "H" in Timeout 1 Time let H := fresh "H" in let x := constr:(let n := 17 in do_n n = do_n n) in let y := (eval lazy in x) in - assert (H := y). (* Finished transaction in 1.19 secs (1.164u,0.024s) (successful) *)
\ No newline at end of file + assert (H := y). (* Finished transaction in 1.19 secs (1.164u,0.024s) (successful) *) diff --git a/test-suite/bugs/closed/3446.v b/test-suite/bugs/closed/3446.v index dce73e1a5..8a0c98c33 100644 --- a/test-suite/bugs/closed/3446.v +++ b/test-suite/bugs/closed/3446.v @@ -48,4 +48,4 @@ Instance isequiv_pr1_contr {A} {P : A -> Type} : IsEquiv (@pr1 A P) | 100. Admitted. Definition path_sigma_hprop {A : Type} {P : A -> Type} (u v : sigT P) : u.1 = v.1 -> u = v := - path_sigma_uncurried P u v o pr1^-1.
\ No newline at end of file + path_sigma_uncurried P u v o pr1^-1. diff --git a/test-suite/bugs/closed/3477.v b/test-suite/bugs/closed/3477.v index e94148647..3ed63604e 100644 --- a/test-suite/bugs/closed/3477.v +++ b/test-suite/bugs/closed/3477.v @@ -6,4 +6,4 @@ Proof. intros A B. evar (a : prod A B); evar (f : (prod A B -> Set)). let a' := (eval unfold a in a) in - set(foo:=eq_refl : a' = (@pair _ _ (fst a') (snd a'))).
\ No newline at end of file + set(foo:=eq_refl : a' = (@pair _ _ (fst a') (snd a'))). diff --git a/test-suite/bugs/closed/3480.v b/test-suite/bugs/closed/3480.v index a81837e71..35e0c51a9 100644 --- a/test-suite/bugs/closed/3480.v +++ b/test-suite/bugs/closed/3480.v @@ -45,4 +45,4 @@ yb : object StrX x : xa <~=~> yb The term "morphism_isomorphic:@morphism (precategory_of_structures P) xa yb" has type "@morphism (precategory_of_structures P) xa yb" -while it is expected to have type "morphism ?40 ?41 ?42". *)
\ No newline at end of file +while it is expected to have type "morphism ?40 ?41 ?42". *) diff --git a/test-suite/bugs/closed/3482.v b/test-suite/bugs/closed/3482.v index 34a5e73da..87fd2723c 100644 --- a/test-suite/bugs/closed/3482.v +++ b/test-suite/bugs/closed/3482.v @@ -8,4 +8,4 @@ Check foo _. (* Toplevel input, characters 6-11: Error: Illegal application (Non-functional construction): The expression "foo" of type "True" cannot be applied to the term - "?36" : "?35" *)
\ No newline at end of file + "?36" : "?35" *) diff --git a/test-suite/bugs/closed/3484.v b/test-suite/bugs/closed/3484.v index dc88a332b..a0e157303 100644 --- a/test-suite/bugs/closed/3484.v +++ b/test-suite/bugs/closed/3484.v @@ -28,4 +28,4 @@ T : Type H : sigT T (fun g : T => paths g g) x : T Unable to unify "paths (@projT1 ?24 ?23 ?25) (@projT1 ?24 ?23 ?26)" with - "paths (projT1 H) (projT1 {| projT1 := x; projT2 := idpath |})". *)
\ No newline at end of file + "paths (projT1 H) (projT1 {| projT1 := x; projT2 := idpath |})". *) diff --git a/test-suite/bugs/closed/3513.v b/test-suite/bugs/closed/3513.v index 9ed0926a6..5adc48215 100644 --- a/test-suite/bugs/closed/3513.v +++ b/test-suite/bugs/closed/3513.v @@ -91,4 +91,4 @@ Debug: 2.2.1.1.1.1: apply ILFun_ILogic on (ILogic OPred) Set Printing All. (* As in 8.5, allow a shelved subgoal to remain *) apply reflexivity. -
\ No newline at end of file + diff --git a/test-suite/bugs/closed/3531.v b/test-suite/bugs/closed/3531.v index 764a7334e..3502b4f54 100644 --- a/test-suite/bugs/closed/3531.v +++ b/test-suite/bugs/closed/3531.v @@ -51,4 +51,4 @@ Goal forall b, (exists e1 e2 e3, admit. admit. Show Universes. -Time Qed.
\ No newline at end of file +Time Qed. diff --git a/test-suite/bugs/closed/3560.v b/test-suite/bugs/closed/3560.v index 65ce4fb6b..a740675f3 100644 --- a/test-suite/bugs/closed/3560.v +++ b/test-suite/bugs/closed/3560.v @@ -12,4 +12,4 @@ Goal forall (A B : Type) (C : Type), Equiv (A -> B -> C) (A * B -> C). Proof. intros. exists (fun u => fun x => u (fst x) (snd x)). -Abort.
\ No newline at end of file +Abort. diff --git a/test-suite/bugs/closed/3561.v b/test-suite/bugs/closed/3561.v index f6cbc9299..ef4422eea 100644 --- a/test-suite/bugs/closed/3561.v +++ b/test-suite/bugs/closed/3561.v @@ -21,4 +21,4 @@ Goal forall (H0 H2 : Type) x p, intros. match goal with | [ |- context[x (?f _)] ] => set(foo':=f) - end.
\ No newline at end of file + end. diff --git a/test-suite/bugs/closed/3567.v b/test-suite/bugs/closed/3567.v index cb16b3ae4..00c9c0546 100644 --- a/test-suite/bugs/closed/3567.v +++ b/test-suite/bugs/closed/3567.v @@ -65,4 +65,4 @@ ap (path_prod_uncurried z0 z') which is ill-typed. Reason is: Pattern-matching expression on an object of inductive type prod has invalid information. - *)
\ No newline at end of file + *) diff --git a/test-suite/bugs/closed/3584.v b/test-suite/bugs/closed/3584.v index 3d4660b48..37fe46376 100644 --- a/test-suite/bugs/closed/3584.v +++ b/test-suite/bugs/closed/3584.v @@ -13,4 +13,4 @@ Definition sum_of_sigT A B (x : sigT (fun b : bool => if b then A else B)) | existT _ false b => inr b end. (* Toplevel input, characters 0-182: Error: Pattern-matching expression on an object of inductive type sigT -has invalid information. *)
\ No newline at end of file +has invalid information. *) diff --git a/test-suite/bugs/closed/3590.v b/test-suite/bugs/closed/3590.v index 3ef9270d4..9fded85a8 100644 --- a/test-suite/bugs/closed/3590.v +++ b/test-suite/bugs/closed/3590.v @@ -9,4 +9,4 @@ Qed. (* Toplevel input, characters 20-58: Error: Failed to get enough information from the left-hand side to type the -right-hand side. *)
\ No newline at end of file +right-hand side. *) diff --git a/test-suite/bugs/closed/3594.v b/test-suite/bugs/closed/3594.v index d1aae7b44..1f86f4bd7 100644 --- a/test-suite/bugs/closed/3594.v +++ b/test-suite/bugs/closed/3594.v @@ -48,4 +48,4 @@ while it is expected to have type object := opposite D; morphism := fun s d : opposite D => morphism (opposite D) d s |}" and "opposite D"). - *)
\ No newline at end of file + *) diff --git a/test-suite/bugs/closed/3596.v b/test-suite/bugs/closed/3596.v index 49dd7be5a..1ee9a5d8c 100644 --- a/test-suite/bugs/closed/3596.v +++ b/test-suite/bugs/closed/3596.v @@ -16,4 +16,4 @@ Goal forall f b, Bar b = Bar b -> Foo f = Foo f. Fail progress unfold Bar. (* success *) Fail progress unfold Foo. (* failed to progress *) reflexivity. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/3618.v b/test-suite/bugs/closed/3618.v index dc560ad52..674b4cc2f 100644 --- a/test-suite/bugs/closed/3618.v +++ b/test-suite/bugs/closed/3618.v @@ -100,4 +100,4 @@ Hint Mode IsEquiv - - + : typeclass_instances. Fail Definition equiv_O_rectnd {fs : Funext} {subU : ReflectiveSubuniverse} (P Q : Type) {Q_inO : inO_internal Q} -: IsEquiv (fun f : O P -> P => compose f (O_unit P)) := _.
\ No newline at end of file +: IsEquiv (fun f : O P -> P => compose f (O_unit P)) := _. diff --git a/test-suite/bugs/closed/3624.v b/test-suite/bugs/closed/3624.v index a05d5eb21..024243cfd 100644 --- a/test-suite/bugs/closed/3624.v +++ b/test-suite/bugs/closed/3624.v @@ -8,4 +8,4 @@ Module Prim. Set Primitive Projections. Class foo (m : Set) := { pf : m = m }. Notation pf' m := (pf (m:=m)). (* Wrong argument name: m. *) -End Prim.
\ No newline at end of file +End Prim. diff --git a/test-suite/bugs/closed/3633.v b/test-suite/bugs/closed/3633.v index 6a952377c..52bb30727 100644 --- a/test-suite/bugs/closed/3633.v +++ b/test-suite/bugs/closed/3633.v @@ -7,4 +7,4 @@ Proof. (* Ensure the constraints are solved independently, otherwise a frozen ?A makes a search for Contr ?A fail when finishing to apply (fun x => x) *) apply (fun x => x), center. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/3638.v b/test-suite/bugs/closed/3638.v index 70144174d..5441fbedc 100644 --- a/test-suite/bugs/closed/3638.v +++ b/test-suite/bugs/closed/3638.v @@ -22,4 +22,4 @@ Goal forall (A B : Type) (x : O A * O B) (x0 : B), (* Toplevel input, characters 15-114: -Anomaly: Bad recursive type. Please report. *)
\ No newline at end of file +Anomaly: Bad recursive type. Please report. *) diff --git a/test-suite/bugs/closed/3640.v b/test-suite/bugs/closed/3640.v index bdbfbb152..5dff98ba2 100644 --- a/test-suite/bugs/closed/3640.v +++ b/test-suite/bugs/closed/3640.v @@ -28,4 +28,4 @@ Proof. simpl in *. Fail match type of H with | _ = negb ?T => unify T (f.1 true); fail 1 "still has f.1 true" - end. (* Error: Tactic failure: still has f.1 true. *)
\ No newline at end of file + end. (* Error: Tactic failure: still has f.1 true. *) diff --git a/test-suite/bugs/closed/3641.v b/test-suite/bugs/closed/3641.v index f47f64ead..730ab3f43 100644 --- a/test-suite/bugs/closed/3641.v +++ b/test-suite/bugs/closed/3641.v @@ -18,4 +18,4 @@ Goal forall (A B : Type) (x : O A * O B) (x0 : B), match goal with | [ |- context[?e] ] => is_evar e; let e' := fresh "e'" in pose (e' := e) end. - Fail change ?g with e'. (* Stack overflow *)
\ No newline at end of file + Fail change ?g with e'. (* Stack overflow *) diff --git a/test-suite/bugs/closed/3648.v b/test-suite/bugs/closed/3648.v index ba6006ed9..58aa16140 100644 --- a/test-suite/bugs/closed/3648.v +++ b/test-suite/bugs/closed/3648.v @@ -80,4 +80,4 @@ Error: Found no subterm matching "F _1 (identity (fst x))" in the current goal. *) rewrite identity_of. (* Toplevel input, characters 15-34: Error: -Found no subterm matching "morphism_of ?202 (identity ?203)" in the current goal. *)
\ No newline at end of file +Found no subterm matching "morphism_of ?202 (identity ?203)" in the current goal. *) diff --git a/test-suite/bugs/closed/3658.v b/test-suite/bugs/closed/3658.v index 622c3c94a..74f4e82db 100644 --- a/test-suite/bugs/closed/3658.v +++ b/test-suite/bugs/closed/3658.v @@ -72,4 +72,4 @@ Module Prim. end. (* Error: Tactic failure: bad H1. *) admit. Defined. -End Prim.
\ No newline at end of file +End Prim. diff --git a/test-suite/bugs/closed/3661.v b/test-suite/bugs/closed/3661.v index fdca49bc4..1f13ffcf3 100644 --- a/test-suite/bugs/closed/3661.v +++ b/test-suite/bugs/closed/3661.v @@ -85,4 +85,4 @@ Goal forall (x3 x9 : PreCategory) (x12 f0 : Functor x9 x3) (@morphism_inverse _ _ _ (@morphism_isomorphic (functor_category x9 x3) f0 x12 x35) _) x37) -*)
\ No newline at end of file +*) diff --git a/test-suite/bugs/closed/3664.v b/test-suite/bugs/closed/3664.v index 63a81b6d0..cd1427a14 100644 --- a/test-suite/bugs/closed/3664.v +++ b/test-suite/bugs/closed/3664.v @@ -21,4 +21,4 @@ Module Prim. Fail progress cbn. (* [cbn] succeeds incorrectly, giving [d x] *) admit. Defined. -End Prim.
\ No newline at end of file +End Prim. diff --git a/test-suite/bugs/closed/3666.v b/test-suite/bugs/closed/3666.v index e69ec1097..c7bc2f22a 100644 --- a/test-suite/bugs/closed/3666.v +++ b/test-suite/bugs/closed/3666.v @@ -48,4 +48,4 @@ H' : H_f a (h c) = H_g b (h c) Unable to unify "hproptype (H_f a (h c))" with "?T (H_f a (h c))". *) Defined. -End Prim.
\ No newline at end of file +End Prim. diff --git a/test-suite/bugs/closed/3668.v b/test-suite/bugs/closed/3668.v index da01ed00e..1add3dba1 100644 --- a/test-suite/bugs/closed/3668.v +++ b/test-suite/bugs/closed/3668.v @@ -51,4 +51,4 @@ Module Prim. end. (* Tactic failure: bad *) all:admit. Defined. -End Prim.
\ No newline at end of file +End Prim. diff --git a/test-suite/bugs/closed/3672.v b/test-suite/bugs/closed/3672.v index 283be4958..b355e7e9d 100644 --- a/test-suite/bugs/closed/3672.v +++ b/test-suite/bugs/closed/3672.v @@ -24,4 +24,4 @@ Record Ar3 C (A:AT) := ; id3 : forall X, ar3 X X }. (* The command has indeed failed with message: => Anomaly: Bad recursive type. Please report. -*)
\ No newline at end of file +*) diff --git a/test-suite/bugs/closed/3698.v b/test-suite/bugs/closed/3698.v index 31de8ec45..3882eee97 100644 --- a/test-suite/bugs/closed/3698.v +++ b/test-suite/bugs/closed/3698.v @@ -23,4 +23,4 @@ Proof. assert (H'' : forall g : X = Y -> (issig_hSet^-1 X).1 = (issig_hSet^-1 Y).1, g = g -> IsEquiv g) by admit. Eval compute in (@projT1 Type IsHSet (@equiv_inv _ _ _ (equiv_isequiv _ _ issig_hSet) X)). - Fail apply H''. (* stack overflow *)
\ No newline at end of file + Fail apply H''. (* stack overflow *) diff --git a/test-suite/bugs/closed/3699.v b/test-suite/bugs/closed/3699.v index efa432526..dbb10f94f 100644 --- a/test-suite/bugs/closed/3699.v +++ b/test-suite/bugs/closed/3699.v @@ -156,4 +156,4 @@ Module Prim. | fail 1 "destruct should generate unfolded projections, as should [let], goal:" G ]. admit. Defined. -End Prim.
\ No newline at end of file +End Prim. diff --git a/test-suite/bugs/closed/3700.v b/test-suite/bugs/closed/3700.v index 4e226524c..bac443e33 100644 --- a/test-suite/bugs/closed/3700.v +++ b/test-suite/bugs/closed/3700.v @@ -81,4 +81,4 @@ Goal (forall x : NonPrim.prod Set Set, match x with NonPrim.pair a b => a = a /\ and (@eq Set (@Prim.fst Set Set x) (@Prim.fst Set Set x)) (@eq Set (@Prim.snd Set Set x) (@Prim.snd Set Set x))) *) Unset Printing All. -Abort.
\ No newline at end of file +Abort. diff --git a/test-suite/bugs/closed/3703.v b/test-suite/bugs/closed/3703.v index 728250076..feeb04d64 100644 --- a/test-suite/bugs/closed/3703.v +++ b/test-suite/bugs/closed/3703.v @@ -29,4 +29,4 @@ Module Keyed. rewrite <- H'. admit. Defined. -End Keyed.
\ No newline at end of file +End Keyed. diff --git a/test-suite/bugs/closed/3732.v b/test-suite/bugs/closed/3732.v index 76beedf68..09f1149c2 100644 --- a/test-suite/bugs/closed/3732.v +++ b/test-suite/bugs/closed/3732.v @@ -102,4 +102,4 @@ cannot be applied to the terms "G0" : "list Type" The 2nd term has type "Type@{Top.53}" which should be coercible to "Type@{Top.12}". - *)
\ No newline at end of file + *) diff --git a/test-suite/bugs/closed/3735.v b/test-suite/bugs/closed/3735.v index a50572ace..aced9615e 100644 --- a/test-suite/bugs/closed/3735.v +++ b/test-suite/bugs/closed/3735.v @@ -1,4 +1,4 @@ Require Import Coq.Program.Tactics. Class Foo := { bar : Type }. Fail Lemma foo : Foo -> bar. (* 'Command has indeed failed.' in both 8.4 and trunk *) -Fail Program Lemma foo : Foo -> bar.
\ No newline at end of file +Fail Program Lemma foo : Foo -> bar. diff --git a/test-suite/bugs/closed/3743.v b/test-suite/bugs/closed/3743.v index c799d4393..ca78987bf 100644 --- a/test-suite/bugs/closed/3743.v +++ b/test-suite/bugs/closed/3743.v @@ -8,4 +8,4 @@ Add Parametric Relation A transitivity proved by transitivity as refine_rel. (* Toplevel input, characters 20-118: -Anomaly: index to an anonymous variable. Please report. *)
\ No newline at end of file +Anomaly: index to an anonymous variable. Please report. *) diff --git a/test-suite/bugs/closed/3753.v b/test-suite/bugs/closed/3753.v index 5bfbee949..f586438cd 100644 --- a/test-suite/bugs/closed/3753.v +++ b/test-suite/bugs/closed/3753.v @@ -1,4 +1,4 @@ Axiom foo : Type -> Type. Axiom bar : forall (T : Type), T -> foo T. Arguments bar A x : rename. -About bar.
\ No newline at end of file +About bar. diff --git a/test-suite/bugs/closed/3782.v b/test-suite/bugs/closed/3782.v index 2dc50c17d..16b0b8b60 100644 --- a/test-suite/bugs/closed/3782.v +++ b/test-suite/bugs/closed/3782.v @@ -61,4 +61,4 @@ The term "e'" has type "@IsEquiv md mc e" while it is expected to have type *) admit. Defined. -End Prim.
\ No newline at end of file +End Prim. diff --git a/test-suite/bugs/closed/3783.v b/test-suite/bugs/closed/3783.v index e21712968..f7e2b5435 100644 --- a/test-suite/bugs/closed/3783.v +++ b/test-suite/bugs/closed/3783.v @@ -30,4 +30,4 @@ Module Prim. Timeout 1 cbv beta in y. (* takes around 2s. Grows with the value passed to [exp] above *) admit. Defined. -End Prim.
\ No newline at end of file +End Prim. diff --git a/test-suite/bugs/closed/3807.v b/test-suite/bugs/closed/3807.v index 108ebf592..a6286f037 100644 --- a/test-suite/bugs/closed/3807.v +++ b/test-suite/bugs/closed/3807.v @@ -30,4 +30,4 @@ Axiom f@{i} : Type@{i}. (* *** [ f@{i} : Type@{i} ] (* i |= *) -*)
\ No newline at end of file +*) diff --git a/test-suite/bugs/closed/3808.v b/test-suite/bugs/closed/3808.v index a5c84e685..ac6a85019 100644 --- a/test-suite/bugs/closed/3808.v +++ b/test-suite/bugs/closed/3808.v @@ -1,3 +1,3 @@ Unset Strict Universe Declaration. Inductive Foo : (let enforce := (fun x => x) : Type@{j} -> Type@{i} in Type@{i}) - := foo : Foo.
\ No newline at end of file + := foo : Foo. diff --git a/test-suite/bugs/closed/3819.v b/test-suite/bugs/closed/3819.v index 355d23a58..0b9c3183c 100644 --- a/test-suite/bugs/closed/3819.v +++ b/test-suite/bugs/closed/3819.v @@ -6,4 +6,4 @@ Lemma test1 (X:Type) : eq (op OpType X) X. Proof eq_refl. Definition test2 (A:Type) : eq (op _ A) A. -Proof eq_refl.
\ No newline at end of file +Proof eq_refl. diff --git a/test-suite/bugs/closed/3881.v b/test-suite/bugs/closed/3881.v index bb6af6a66..7c60ddf34 100644 --- a/test-suite/bugs/closed/3881.v +++ b/test-suite/bugs/closed/3881.v @@ -32,4 +32,4 @@ Proof. apply (@isequiv_homotopic _ _ ((g o f) o f^-1) g _ (fun b => ap g (eisretr f b))). Qed. -
\ No newline at end of file + diff --git a/test-suite/bugs/closed/3886.v b/test-suite/bugs/closed/3886.v index 2ac4abe54..b523b117e 100644 --- a/test-suite/bugs/closed/3886.v +++ b/test-suite/bugs/closed/3886.v @@ -20,4 +20,4 @@ Obligation 1 of doubleO. apply cheat. Qed. -Check doubleE.
\ No newline at end of file +Check doubleE. diff --git a/test-suite/bugs/closed/3899.v b/test-suite/bugs/closed/3899.v index e83166aae..7754934c0 100644 --- a/test-suite/bugs/closed/3899.v +++ b/test-suite/bugs/closed/3899.v @@ -8,4 +8,4 @@ Fail Check fun x y : unit => eq_refl : x = y. Record ok : Set := tt' { a : unit }. Record nonprim : Prop := { undef : unit }. -Record prim : Prop := { def : True }.
\ No newline at end of file +Record prim : Prop := { def : True }. diff --git a/test-suite/bugs/closed/3943.v b/test-suite/bugs/closed/3943.v index 5e5ba816f..ac9c50369 100644 --- a/test-suite/bugs/closed/3943.v +++ b/test-suite/bugs/closed/3943.v @@ -47,4 +47,4 @@ Definition path_isomorphic (i j : Isomorphic s d) Admitted. Definition ap_morphism_inverse_path_isomorphic (i j : Isomorphic s d) p q -: ap (fun e : Isomorphic s d => e^-1)%morphism (path_isomorphic i j p) = q.
\ No newline at end of file +: ap (fun e : Isomorphic s d => e^-1)%morphism (path_isomorphic i j p) = q. diff --git a/test-suite/bugs/closed/3956.v b/test-suite/bugs/closed/3956.v index 66dee702a..4957cc740 100644 --- a/test-suite/bugs/closed/3956.v +++ b/test-suite/bugs/closed/3956.v @@ -140,4 +140,4 @@ Module Comodality_Theory (F : Comodality). End cip_FPHM. End isequiv_F_prod_cmp_M. -End Comodality_Theory.
\ No newline at end of file +End Comodality_Theory. diff --git a/test-suite/bugs/closed/3960.v b/test-suite/bugs/closed/3960.v index e56dcef74..352731248 100644 --- a/test-suite/bugs/closed/3960.v +++ b/test-suite/bugs/closed/3960.v @@ -23,4 +23,4 @@ Class myClassP (A : Type) := Instance myInstanceP : myClassP nat := { barP := fooP - }.
\ No newline at end of file + }. diff --git a/test-suite/bugs/closed/3974.v b/test-suite/bugs/closed/3974.v index b6be15959..3d9e06b61 100644 --- a/test-suite/bugs/closed/3974.v +++ b/test-suite/bugs/closed/3974.v @@ -4,4 +4,4 @@ End S. Module Type M (X : S). Fail Module P (X : S). (* Used to say: Anomaly: X already exists. Please report. *) - (* Should rather say now: Error: X already exists. *)
\ No newline at end of file + (* Should rather say now: Error: X already exists. *) diff --git a/test-suite/bugs/closed/3975.v b/test-suite/bugs/closed/3975.v index 95851c813..c7616b3ab 100644 --- a/test-suite/bugs/closed/3975.v +++ b/test-suite/bugs/closed/3975.v @@ -5,4 +5,4 @@ Module M (X:S). End M. Module Type P (X : S). Print M. (* Used to say: Anomaly: X already exists. Please report. *) - (* Should rather : print something :-) *)
\ No newline at end of file + (* Should rather : print something :-) *) diff --git a/test-suite/bugs/closed/3998.v b/test-suite/bugs/closed/3998.v index ced13839d..e17550e90 100644 --- a/test-suite/bugs/closed/3998.v +++ b/test-suite/bugs/closed/3998.v @@ -21,4 +21,4 @@ Axiom ex : RecordOf _ I1FieldType. Definition works := (fun ex' => update ex' C true) (update ex C false). Set Typeclasses Debug. -Definition doesnt := update (update ex C false) C true.
\ No newline at end of file +Definition doesnt := update (update ex C false) C true. diff --git a/test-suite/bugs/closed/4031.v b/test-suite/bugs/closed/4031.v index 2b8641ebb..6c23baffa 100644 --- a/test-suite/bugs/closed/4031.v +++ b/test-suite/bugs/closed/4031.v @@ -11,4 +11,4 @@ Proof. change mytt with (@something _ mytt) in x. subst x. (* Proof works if this line is removed *) reflexivity. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/4069.v b/test-suite/bugs/closed/4069.v index 61527764e..606c6e084 100644 --- a/test-suite/bugs/closed/4069.v +++ b/test-suite/bugs/closed/4069.v @@ -101,4 +101,4 @@ Variable T : Type. Goal @eq Type T T. congruence. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/4095.v b/test-suite/bugs/closed/4095.v index ffd33d381..8d7dfbd49 100644 --- a/test-suite/bugs/closed/4095.v +++ b/test-suite/bugs/closed/4095.v @@ -84,4 +84,4 @@ O1 : T -> PointedOPred tr : T -> T O2 : PointedOPred x0 : T -H : forall x0 : T, catOP (O0 x0) (O1 (tr x0)) |-- O1 x0 *)
\ No newline at end of file +H : forall x0 : T, catOP (O0 x0) (O1 (tr x0)) |-- O1 x0 *) diff --git a/test-suite/bugs/closed/4097.v b/test-suite/bugs/closed/4097.v index 02aa25e09..183b860d1 100644 --- a/test-suite/bugs/closed/4097.v +++ b/test-suite/bugs/closed/4097.v @@ -62,4 +62,4 @@ Definition path_path_sigma {A : Type} (P : A -> Type) (u v : sigT P) (r : p..1 = q..1) (s : transport (fun x => transport P x u.2 = v.2) r p..2 = q..2) : p = q - := path_path_sigma_uncurried P u v p q (r; s).
\ No newline at end of file + := path_path_sigma_uncurried P u v p q (r; s). diff --git a/test-suite/bugs/closed/4101.v b/test-suite/bugs/closed/4101.v index a38b05096..75a26a067 100644 --- a/test-suite/bugs/closed/4101.v +++ b/test-suite/bugs/closed/4101.v @@ -16,4 +16,4 @@ Lemma sigT_obj_eq Proof. intros. Set Debug Tactic Unification. - apply path_forall.
\ No newline at end of file + apply path_forall. diff --git a/test-suite/bugs/closed/4120.v b/test-suite/bugs/closed/4120.v index 00db8f7f3..315dc0d24 100644 --- a/test-suite/bugs/closed/4120.v +++ b/test-suite/bugs/closed/4120.v @@ -2,4 +2,4 @@ Definition id {T} (x : T) := x. Goal sigT (fun x => id x)%type. change (fun x => ?f x) with f. exists Type. exact Set. -Defined. (* Error: Attempt to save a proof with shelved goals (in proof Unnamed_thm) *)
\ No newline at end of file +Defined. (* Error: Attempt to save a proof with shelved goals (in proof Unnamed_thm) *) diff --git a/test-suite/bugs/closed/4151.v b/test-suite/bugs/closed/4151.v index fec64555f..fc0b58cfe 100644 --- a/test-suite/bugs/closed/4151.v +++ b/test-suite/bugs/closed/4151.v @@ -400,4 +400,4 @@ Section sound. Undo. assumption. Undo. - eassumption. (* no applicable tactic *)
\ No newline at end of file + eassumption. (* no applicable tactic *) diff --git a/test-suite/bugs/closed/4161.v b/test-suite/bugs/closed/4161.v index aa2b189b6..d2003ab1f 100644 --- a/test-suite/bugs/closed/4161.v +++ b/test-suite/bugs/closed/4161.v @@ -24,4 +24,4 @@ Inductive t : Type -> Type := Fixpoint test {A : Type} (x : t A) : t (A + unit) := match x in t A with | Just B x => @test B x - end.
\ No newline at end of file + end. diff --git a/test-suite/bugs/closed/4203.v b/test-suite/bugs/closed/4203.v index 076a3c3d6..eb6867a03 100644 --- a/test-suite/bugs/closed/4203.v +++ b/test-suite/bugs/closed/4203.v @@ -16,4 +16,4 @@ Definition t' := Eval vm_compute in constant_ok nat_ops nat_ops_ok. Definition t'' := Eval native_compute in constant_ok nat_ops nat_ops_ok. Check (eq_refl t : t = t'). -Check (eq_refl t : t = t'').
\ No newline at end of file +Check (eq_refl t : t = t''). diff --git a/test-suite/bugs/closed/4214.v b/test-suite/bugs/closed/4214.v index d684e8cf4..2e620fce2 100644 --- a/test-suite/bugs/closed/4214.v +++ b/test-suite/bugs/closed/4214.v @@ -3,4 +3,4 @@ Goal forall A (a b c : A), b = a -> b = c -> a = c. intros. subst. reflexivity. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/4250.v b/test-suite/bugs/closed/4250.v index 74cacf559..f5d0d1a52 100644 --- a/test-suite/bugs/closed/4250.v +++ b/test-suite/bugs/closed/4250.v @@ -8,4 +8,4 @@ Function f2 {A:Type} {n:nat} {v:Vector.t A n} : nat := n. (* fails with "The reference A was not found in the current environment." *) Function f3 `{n:nat , u:Vector.t A n} := u. -Check R_f3_complete.
\ No newline at end of file +Check R_f3_complete. diff --git a/test-suite/bugs/closed/4251.v b/test-suite/bugs/closed/4251.v index 66343d667..f112e7b4d 100644 --- a/test-suite/bugs/closed/4251.v +++ b/test-suite/bugs/closed/4251.v @@ -14,4 +14,4 @@ Check array Type. Check fun A : Type => Ref A. Definition abs_val (a : Type) := - bind (ref a) (fun r : array Type => array_make tt).
\ No newline at end of file + bind (ref a) (fun r : array Type => array_make tt). diff --git a/test-suite/bugs/closed/4273.v b/test-suite/bugs/closed/4273.v index 591ea4b5b..401e86649 100644 --- a/test-suite/bugs/closed/4273.v +++ b/test-suite/bugs/closed/4273.v @@ -6,4 +6,4 @@ Theorem onefiber' (q : total2 (fun y => y = 0)) : True. Proof. assert (foo:=pr2 _ q). simpl in foo. destruct foo. (* Error: q is used in conclusion. *) exact I. Qed. -Print onefiber'.
\ No newline at end of file +Print onefiber'. diff --git a/test-suite/bugs/closed/4276.v b/test-suite/bugs/closed/4276.v index ba82e6c37..ea9cbb210 100644 --- a/test-suite/bugs/closed/4276.v +++ b/test-suite/bugs/closed/4276.v @@ -8,4 +8,4 @@ Definition bad' : True := mybox.(unwrap _ _). Fail Definition bad : False := unwrap _ _ mybox. -(* Closed under the global context *)
\ No newline at end of file +(* Closed under the global context *) diff --git a/test-suite/bugs/closed/4287.v b/test-suite/bugs/closed/4287.v index 43c9b5129..757b71b2d 100644 --- a/test-suite/bugs/closed/4287.v +++ b/test-suite/bugs/closed/4287.v @@ -120,4 +120,4 @@ Definition setle (B : Type@{i}) := Fail Check @setlt@{j Prop}. Fail Definition foo := @setle@{j Prop}. Check setlt@{Set i}. -Check setlt@{Set j}.
\ No newline at end of file +Check setlt@{Set j}. diff --git a/test-suite/bugs/closed/4293.v b/test-suite/bugs/closed/4293.v index 3671c931b..21d333fa6 100644 --- a/test-suite/bugs/closed/4293.v +++ b/test-suite/bugs/closed/4293.v @@ -4,4 +4,4 @@ End Foo. Module M : Foo. Definition T := let X := Type in Type. -End M.
\ No newline at end of file +End M. diff --git a/test-suite/bugs/closed/4299.v b/test-suite/bugs/closed/4299.v index 955c3017d..a1daa193a 100644 --- a/test-suite/bugs/closed/4299.v +++ b/test-suite/bugs/closed/4299.v @@ -9,4 +9,4 @@ End Foo. Module M : Foo with Definition U := Type : Type. Definition U := let X := Type in Type. Definition eq : Type = U := eq_refl. -Fail End M.
\ No newline at end of file +Fail End M. diff --git a/test-suite/bugs/closed/4306.v b/test-suite/bugs/closed/4306.v index 4aef5bb95..28f028ad8 100644 --- a/test-suite/bugs/closed/4306.v +++ b/test-suite/bugs/closed/4306.v @@ -29,4 +29,4 @@ Function bar (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) | Eq => x :: foo (xs', ys') | Gt => y :: foo (xs, ys') end - end.
\ No newline at end of file + end. diff --git a/test-suite/bugs/closed/4328.v b/test-suite/bugs/closed/4328.v index 8e1bb3100..b40b3a483 100644 --- a/test-suite/bugs/closed/4328.v +++ b/test-suite/bugs/closed/4328.v @@ -3,4 +3,4 @@ Axiom pi : forall (P : Prop) (p : P), Prop. Definition test1 A (x : _) := pi A x. (* success *) Fail Definition test2 A (x : A) := pi A x. (* failure ??? *) Fail Definition test3 A (x : A) (_ : M A) := pi A x. (* failure *) -Fail Definition test4 A (_ : M A) (x : A) := pi A x. (* success ??? *)
\ No newline at end of file +Fail Definition test4 A (_ : M A) (x : A) := pi A x. (* success ??? *) diff --git a/test-suite/bugs/closed/4354.v b/test-suite/bugs/closed/4354.v index e71ddaf71..c55b4cf02 100644 --- a/test-suite/bugs/closed/4354.v +++ b/test-suite/bugs/closed/4354.v @@ -8,4 +8,4 @@ Proof. auto using closed_increment. Show Universes. Qed. (* also fails with -nois, so the content of the hint database does not matter -*)
\ No newline at end of file +*) diff --git a/test-suite/bugs/closed/4375.v b/test-suite/bugs/closed/4375.v index 71e3a7518..468bade1c 100644 --- a/test-suite/bugs/closed/4375.v +++ b/test-suite/bugs/closed/4375.v @@ -104,4 +104,4 @@ with cb@{i} (t : Type@{i}) : foo@{i} t := Print ca. Print cb. -
\ No newline at end of file + diff --git a/test-suite/bugs/closed/4416.v b/test-suite/bugs/closed/4416.v index 3189685ec..62b90b428 100644 --- a/test-suite/bugs/closed/4416.v +++ b/test-suite/bugs/closed/4416.v @@ -1,4 +1,4 @@ Goal exists x, x. Unset Solve Unification Constraints. unshelve refine (ex_intro _ _ _); match goal with _ => refine (_ _) end. -(* Error: Incorrect number of goals (expected 2 tactics). *)
\ No newline at end of file +(* Error: Incorrect number of goals (expected 2 tactics). *) diff --git a/test-suite/bugs/closed/4433.v b/test-suite/bugs/closed/4433.v index 9eeb86468..83c0e3f81 100644 --- a/test-suite/bugs/closed/4433.v +++ b/test-suite/bugs/closed/4433.v @@ -26,4 +26,4 @@ Proof. case proof_admitted. Unshelve. all:constructor. -Defined.
\ No newline at end of file +Defined. diff --git a/test-suite/bugs/closed/4443.v b/test-suite/bugs/closed/4443.v index 66dfa0e68..a3a8717d9 100644 --- a/test-suite/bugs/closed/4443.v +++ b/test-suite/bugs/closed/4443.v @@ -28,4 +28,4 @@ Defined. Set Printing Universes. Check PROD@{i i i}. Check PRODinj@{i j}. -Fail Check PRODinj@{j i}.
\ No newline at end of file +Fail Check PRODinj@{j i}. diff --git a/test-suite/bugs/closed/4450.v b/test-suite/bugs/closed/4450.v index ecebaba81..c1fe44315 100644 --- a/test-suite/bugs/closed/4450.v +++ b/test-suite/bugs/closed/4450.v @@ -55,4 +55,4 @@ Proof. eauto using foo. Show Universes. Undo. eauto using foop. Show Proof. Show Universes. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/4480.v b/test-suite/bugs/closed/4480.v index 08a86330f..98c05ee1a 100644 --- a/test-suite/bugs/closed/4480.v +++ b/test-suite/bugs/closed/4480.v @@ -9,4 +9,4 @@ Admitted. Goal True. Fail setoid_rewrite foo. Fail setoid_rewrite trueI. -
\ No newline at end of file + diff --git a/test-suite/bugs/closed/4498.v b/test-suite/bugs/closed/4498.v index ccdb2dddd..379e46b3e 100644 --- a/test-suite/bugs/closed/4498.v +++ b/test-suite/bugs/closed/4498.v @@ -21,4 +21,4 @@ Require Export Coq.Setoids.Setoid. Add Parametric Morphism `{C : Category} {A B C} : (@compose _ A B C) with signature equiv ==> equiv ==> equiv as compose_mor. -Proof. apply comp_respects. Qed.
\ No newline at end of file +Proof. apply comp_respects. Qed. diff --git a/test-suite/bugs/closed/4503.v b/test-suite/bugs/closed/4503.v index f54d6433d..5162f352d 100644 --- a/test-suite/bugs/closed/4503.v +++ b/test-suite/bugs/closed/4503.v @@ -34,4 +34,4 @@ Section Embed_ILogic_Pre. Polymorphic Universes A T. Fail Context {A : Type@{A}} {ILA: ILogic.ILogic@{A} A}. -End Embed_ILogic_Pre.
\ No newline at end of file +End Embed_ILogic_Pre. diff --git a/test-suite/bugs/closed/4519.v b/test-suite/bugs/closed/4519.v index ccbc47d20..945183fae 100644 --- a/test-suite/bugs/closed/4519.v +++ b/test-suite/bugs/closed/4519.v @@ -18,4 +18,4 @@ Check qux nat nat nat : Set. Check qux nat nat Set : Set. (* Error: The term "qux@{Top.50 Top.51} ?T ?T0 Set" has type "Type@{Top.50}" while it is expected to have type "Set" -(universe inconsistency: Cannot enforce Top.50 = Set because Set < Top.50). *)
\ No newline at end of file +(universe inconsistency: Cannot enforce Top.50 = Set because Set < Top.50). *) diff --git a/test-suite/bugs/closed/4603.v b/test-suite/bugs/closed/4603.v index e7567623a..2c90044dc 100644 --- a/test-suite/bugs/closed/4603.v +++ b/test-suite/bugs/closed/4603.v @@ -7,4 +7,4 @@ Abort. Goal True. Definition foo (A : Type) : Prop:= True. set (x:=foo). split. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/4627.v b/test-suite/bugs/closed/4627.v index e1206bb37..4f56e1958 100644 --- a/test-suite/bugs/closed/4627.v +++ b/test-suite/bugs/closed/4627.v @@ -46,4 +46,4 @@ The term "predicate nat (Build_sa nat)" has type while it is expected to have type "Type@{Top.208}" (universe inconsistency: Cannot enforce Top.205 <= Top.208 because Top.208 < Top.205). -*)
\ No newline at end of file +*) diff --git a/test-suite/bugs/closed/4679.v b/test-suite/bugs/closed/4679.v index c94fa31a9..3f41c5d6b 100644 --- a/test-suite/bugs/closed/4679.v +++ b/test-suite/bugs/closed/4679.v @@ -15,4 +15,4 @@ Proof. Undo. setoid_rewrite H. (* Error: Tactic failure: setoid rewrite failed: Nothing to rewrite. *) reflexivity. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/4723.v b/test-suite/bugs/closed/4723.v index 888481210..5fb9696f3 100644 --- a/test-suite/bugs/closed/4723.v +++ b/test-suite/bugs/closed/4723.v @@ -25,4 +25,4 @@ Program Fact kp_assoc (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc): kp x (kp y z) = kp (kp x y) z. admit. -Admitted.
\ No newline at end of file +Admitted. diff --git a/test-suite/bugs/closed/4754.v b/test-suite/bugs/closed/4754.v index 5bb3cd1be..67d645a68 100644 --- a/test-suite/bugs/closed/4754.v +++ b/test-suite/bugs/closed/4754.v @@ -32,4 +32,4 @@ Proof. pose proof (_ : (Proper (_ ==> eq ==> _) and)). setoid_rewrite (FG _ _); [ | reflexivity.. ]. Undo. - setoid_rewrite (FG _ eq_refl). (* Error: Tactic failure: setoid rewrite failed: Nothing to rewrite. in 8.5 *) Admitted.
\ No newline at end of file + setoid_rewrite (FG _ eq_refl). (* Error: Tactic failure: setoid rewrite failed: Nothing to rewrite. in 8.5 *) Admitted. diff --git a/test-suite/bugs/closed/4763.v b/test-suite/bugs/closed/4763.v index ae8ed0e6e..9613b5c24 100644 --- a/test-suite/bugs/closed/4763.v +++ b/test-suite/bugs/closed/4763.v @@ -10,4 +10,4 @@ Goal forall x y z, leb x y -> leb y z -> True. => pose proof (transitivity H H' : is_true (R x z)) end. exact I. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/4769.v b/test-suite/bugs/closed/4769.v index 33a1d1a50..f0c91f7b4 100644 --- a/test-suite/bugs/closed/4769.v +++ b/test-suite/bugs/closed/4769.v @@ -91,4 +91,4 @@ Section Adjunction. (oppositeC C) D C (identityF (oppositeC C)) G)) }. -End Adjunction.
\ No newline at end of file +End Adjunction. diff --git a/test-suite/bugs/closed/4869.v b/test-suite/bugs/closed/4869.v index 6d21b66fe..ac5d7ea28 100644 --- a/test-suite/bugs/closed/4869.v +++ b/test-suite/bugs/closed/4869.v @@ -15,4 +15,4 @@ Section Foo. Constraint Set < j. Definition foo := Type@{j}. -End Foo.
\ No newline at end of file +End Foo. diff --git a/test-suite/bugs/closed/4873.v b/test-suite/bugs/closed/4873.v index f2f917b4e..3be36d847 100644 --- a/test-suite/bugs/closed/4873.v +++ b/test-suite/bugs/closed/4873.v @@ -69,4 +69,4 @@ Proof. destruct xs; simpl; intros; subst; auto. generalize dependent t. simpl in *. induction xs; simpl in *; intros; congruence. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/4877.v b/test-suite/bugs/closed/4877.v index 7e3c78dc2..7d153d982 100644 --- a/test-suite/bugs/closed/4877.v +++ b/test-suite/bugs/closed/4877.v @@ -9,4 +9,4 @@ Ltac induction_last := Goal forall n m : nat, True -> n = m -> m = n. induction_last. reflexivity. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/5036.v b/test-suite/bugs/closed/5036.v index 12c958be6..83f167745 100644 --- a/test-suite/bugs/closed/5036.v +++ b/test-suite/bugs/closed/5036.v @@ -7,4 +7,4 @@ Section foo. autorewrite with core. constructor. Qed. -End foo. (* Anomaly: Universe Top.16 undefined. Please report. *)
\ No newline at end of file +End foo. (* Anomaly: Universe Top.16 undefined. Please report. *) diff --git a/test-suite/bugs/closed/5065.v b/test-suite/bugs/closed/5065.v index 6bd677ba6..932fee8b3 100644 --- a/test-suite/bugs/closed/5065.v +++ b/test-suite/bugs/closed/5065.v @@ -3,4 +3,4 @@ Inductive foo := C1 : bar -> foo with bar := C2 : foo -> bar. Lemma L1 : foo -> True with L2 : bar -> True. intros; clear L1 L2; abstract (exact I). intros; exact I. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/5123.v b/test-suite/bugs/closed/5123.v index bcde510ee..17231bffc 100644 --- a/test-suite/bugs/closed/5123.v +++ b/test-suite/bugs/closed/5123.v @@ -30,4 +30,4 @@ Goal True. all:cycle 3. eapply existT. (*This does no typeclass resultion, which is correct.*) Focus 5. -Abort.
\ No newline at end of file +Abort. diff --git a/test-suite/bugs/closed/5180.v b/test-suite/bugs/closed/5180.v index 261092ee6..05603a048 100644 --- a/test-suite/bugs/closed/5180.v +++ b/test-suite/bugs/closed/5180.v @@ -61,4 +61,4 @@ The term "x" has type "TypeOfTypei' (Typei 0)" while it is expected to have type "TypeOfTypei' (Typei 1)" (universe inconsistency: Cannot enforce b = a because a < b). *) all:compute in *. - all:exact x.
\ No newline at end of file + all:exact x. diff --git a/test-suite/bugs/closed/5203.v b/test-suite/bugs/closed/5203.v index ed137395f..3428e1a45 100644 --- a/test-suite/bugs/closed/5203.v +++ b/test-suite/bugs/closed/5203.v @@ -2,4 +2,4 @@ Goal True. Typeclasses eauto := debug. Fail solve [ typeclasses eauto ]. Fail typeclasses eauto. -
\ No newline at end of file + diff --git a/test-suite/bugs/closed/5315.v b/test-suite/bugs/closed/5315.v index f1f1b8c05..d8824bff8 100644 --- a/test-suite/bugs/closed/5315.v +++ b/test-suite/bugs/closed/5315.v @@ -7,4 +7,4 @@ Function dumb_nope (a:nat) {struct a} := match (id (fun x => x)) a with O => O | S n' => dumb_nope n' end. (* This check is just present to ensure Function worked well *) -Check R_dumb_nope_complete.
\ No newline at end of file +Check R_dumb_nope_complete. diff --git a/test-suite/bugs/closed/5578.v b/test-suite/bugs/closed/5578.v index 5bcdaa2f1..b9f0bc45c 100644 --- a/test-suite/bugs/closed/5578.v +++ b/test-suite/bugs/closed/5578.v @@ -54,4 +54,4 @@ Goal forall (Rat : Set) (PositiveMap_t : Set -> Set) f eta ( (Bind (k eta) (fun rands => ret_bool (interp_term_fixed_t_x eta (adv' eta) rands ?= interp_term_fixed_t_x eta (adv' eta) rands)))))). - (* Error: Anomaly "Signature and its instance do not match." Please report at http://coq.inria.fr/bugs/. *)
\ No newline at end of file + (* Error: Anomaly "Signature and its instance do not match." Please report at http://coq.inria.fr/bugs/. *) diff --git a/test-suite/bugs/closed/5618.v b/test-suite/bugs/closed/5618.v index ab88a88f4..47e0e92d2 100644 --- a/test-suite/bugs/closed/5618.v +++ b/test-suite/bugs/closed/5618.v @@ -6,4 +6,4 @@ Function test {T} (v : T) (x : nat) : nat := | S x' => test v x' end. -Check R_test_complete.
\ No newline at end of file +Check R_test_complete. diff --git a/test-suite/bugs/closed/808_2411.v b/test-suite/bugs/closed/808_2411.v index 1c13e7454..1169b2036 100644 --- a/test-suite/bugs/closed/808_2411.v +++ b/test-suite/bugs/closed/808_2411.v @@ -24,4 +24,4 @@ rewrite bar'. now apply le_S. Qed. -End test.
\ No newline at end of file +End test. diff --git a/test-suite/bugs/closed/HoTT_coq_014.v b/test-suite/bugs/closed/HoTT_coq_014.v index 223a98de1..5c4503664 100644 --- a/test-suite/bugs/closed/HoTT_coq_014.v +++ b/test-suite/bugs/closed/HoTT_coq_014.v @@ -199,4 +199,4 @@ Fail Admitted. Polymorphic Definition UnderlyingGraphFunctor_MorphismOf (C D : SmallCategory) (F : SpecializedFunctor C D) : Morphism (FunctorCategory GraphIndexingCategory TypeCat) (UnderlyingGraph C) (UnderlyingGraph D). (* Anomaly: apply_coercion. Please report.*) Proof. -Admitted.
\ No newline at end of file +Admitted. diff --git a/test-suite/bugs/closed/HoTT_coq_080.v b/test-suite/bugs/closed/HoTT_coq_080.v index 6b07c3040..a9e0bd267 100644 --- a/test-suite/bugs/closed/HoTT_coq_080.v +++ b/test-suite/bugs/closed/HoTT_coq_080.v @@ -24,4 +24,4 @@ Goal forall C D (x y : ob (sum_category C D)), Type. intros C D x y. hnf in x, y. exact (hom (sum_category _ _) x y). -Defined.
\ No newline at end of file +Defined. 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. diff --git a/test-suite/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v index 7906a5b15..d63a3548e 100644 --- a/test-suite/coqchk/cumulativity.v +++ b/test-suite/coqchk/cumulativity.v @@ -64,4 +64,4 @@ I disable these tests because cqochk can't process them when compiled with (* Inductive TP2 := tp2 : Type@{i} -> Type@{j} -> TP2. *) -(* End subtyping_test. *)
\ No newline at end of file +(* End subtyping_test. *) diff --git a/test-suite/failure/circular_subtyping.v b/test-suite/failure/circular_subtyping.v index ceccd4607..9eb7e3bc2 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 cb39893f4..d193dc484 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 eda4a1867..3ae877054 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 2b3cf1066..3d2eef6a9 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 +*) diff --git a/test-suite/ideal-features/implicit_binders.v b/test-suite/ideal-features/implicit_binders.v index 2ec727808..d75620c25 100644 --- a/test-suite/ideal-features/implicit_binders.v +++ b/test-suite/ideal-features/implicit_binders.v @@ -121,4 +121,4 @@ Definition qux₁ {( F : `(SomeStruct a) )} : nat := 0. (** *** Questions - Autres propositions de syntaxe ? - Réactions sur la construction ? - *)
\ No newline at end of file + *) diff --git a/test-suite/interactive/ParalITP.v b/test-suite/interactive/ParalITP.v index a96d4a5c7..7fab2a58e 100644 --- a/test-suite/interactive/ParalITP.v +++ b/test-suite/interactive/ParalITP.v @@ -44,4 +44,4 @@ split. exact a. Qed. -End Demo.
\ No newline at end of file +End Demo. diff --git a/test-suite/interactive/proof_block.v b/test-suite/interactive/proof_block.v index 31e349376..a865632e8 100644 --- a/test-suite/interactive/proof_block.v +++ b/test-suite/interactive/proof_block.v @@ -63,4 +63,4 @@ split. split. split. - solve [ trivial ]. - solve [ trivial ]. - exact 6. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/modules/Demo.v b/test-suite/modules/Demo.v index 1f27fe1ba..820fda172 100644 --- a/test-suite/modules/Demo.v +++ b/test-suite/modules/Demo.v @@ -52,4 +52,4 @@ Print N'''.x. Import N'''. -Print t.
\ No newline at end of file +Print t. diff --git a/test-suite/modules/Nat.v b/test-suite/modules/Nat.v index 57878a5f1..d2116d218 100644 --- a/test-suite/modules/Nat.v +++ b/test-suite/modules/Nat.v @@ -16,4 +16,4 @@ Qed. Lemma le_antis : forall n m : nat, le n m -> le m n -> n = m. eauto with arith. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v index 6198f29a0..8ba8525c6 100644 --- a/test-suite/modules/PO.v +++ b/test-suite/modules/PO.v @@ -54,4 +54,4 @@ Module NN := Pair Nat Nat. Lemma zz_min : forall p : NN.T, NN.le (0, 0) p. info auto with arith. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/modules/Tescik.v b/test-suite/modules/Tescik.v index 1d1b1e0ab..ea4955394 100644 --- a/test-suite/modules/Tescik.v +++ b/test-suite/modules/Tescik.v @@ -27,4 +27,4 @@ Module List (X: ELEM). End List. -Module N := List Nat.
\ No newline at end of file +Module N := List Nat. diff --git a/test-suite/modules/grammar.v b/test-suite/modules/grammar.v index 9657c685d..11ad205e4 100644 --- a/test-suite/modules/grammar.v +++ b/test-suite/modules/grammar.v @@ -12,4 +12,4 @@ Check (f 0 0). Check (f 0 0). Import M. Check (f 0 0). -Check (N.f 0 0).
\ No newline at end of file +Check (N.f 0 0). diff --git a/test-suite/modules/injection_discriminate_inversion.v b/test-suite/modules/injection_discriminate_inversion.v index d4ac7b3a2..8b5969dd7 100644 --- a/test-suite/modules/injection_discriminate_inversion.v +++ b/test-suite/modules/injection_discriminate_inversion.v @@ -31,4 +31,4 @@ Goal forall x, M.C x = M1.C 0 -> x = 0. par des modules differents *) inversion H. reflexivity. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/modules/modeq.v b/test-suite/modules/modeq.v index 1238ee9de..c8129eec5 100644 --- a/test-suite/modules/modeq.v +++ b/test-suite/modules/modeq.v @@ -19,4 +19,4 @@ Module Z. Module N := M. End Z. -Module A : SIG := Z.
\ No newline at end of file +Module A : SIG := Z. diff --git a/test-suite/modules/pliczek.v b/test-suite/modules/pliczek.v index f806a7c41..51f5f4007 100644 --- a/test-suite/modules/pliczek.v +++ b/test-suite/modules/pliczek.v @@ -1,3 +1,3 @@ Require Export plik. -Definition tutu (X : Set) := toto X.
\ No newline at end of file +Definition tutu (X : Set) := toto X. diff --git a/test-suite/modules/plik.v b/test-suite/modules/plik.v index 50bfd9604..c2f0fe3ce 100644 --- a/test-suite/modules/plik.v +++ b/test-suite/modules/plik.v @@ -1,3 +1,3 @@ Definition toto (x : Set) := x. -(* <Warning> : Grammar is replaced by Notation *)
\ No newline at end of file +(* <Warning> : Grammar is replaced by Notation *) diff --git a/test-suite/modules/pseudo_circular_with.v b/test-suite/modules/pseudo_circular_with.v index 9e46d17ed..6bf067fd1 100644 --- a/test-suite/modules/pseudo_circular_with.v +++ b/test-suite/modules/pseudo_circular_with.v @@ -3,4 +3,4 @@ Module Type T. Declare Module M:S. End T. Module N:S. End N. Module NN:T. Module M:=N. End NN. -Module Type U := T with Module M:=NN.
\ No newline at end of file +Module Type U := T with Module M:=NN. diff --git a/test-suite/modules/sig.v b/test-suite/modules/sig.v index da5d25fa2..fc936a515 100644 --- a/test-suite/modules/sig.v +++ b/test-suite/modules/sig.v @@ -26,4 +26,4 @@ Module Type SIG. Parameter x : T. End SIG. -Module J : SIG := M.N.
\ No newline at end of file +Module J : SIG := M.N. diff --git a/test-suite/output/CompactContexts.v b/test-suite/output/CompactContexts.v index 07588d34f..c409c0ee4 100644 --- a/test-suite/output/CompactContexts.v +++ b/test-suite/output/CompactContexts.v @@ -2,4 +2,4 @@ Set Printing Compact Contexts. Lemma f (hP1:True) (a:nat) (b:list nat) (h:forall (x:nat) , { y:nat | y > x}) (h2:True): False. Show. -Abort.
\ No newline at end of file +Abort. diff --git a/test-suite/output/SearchPattern.v b/test-suite/output/SearchPattern.v index bde195a51..de9f48873 100644 --- a/test-suite/output/SearchPattern.v +++ b/test-suite/output/SearchPattern.v @@ -33,4 +33,4 @@ Goal forall n (P:nat -> Prop), P n -> ~P n -> False. Search (P _) -"h'". (* search hypothesis also for patterns *) Search (P _) -not. (* search hypothesis also for patterns *) -Abort.
\ No newline at end of file +Abort. diff --git a/test-suite/output/ltac_missing_args.v b/test-suite/output/ltac_missing_args.v index 8ecd97aa5..91331a1de 100644 --- a/test-suite/output/ltac_missing_args.v +++ b/test-suite/output/ltac_missing_args.v @@ -16,4 +16,4 @@ Goal True. Fail (fun _ => idtac). Fail rec True. Fail let rec tac x := tac in tac True. -Abort.
\ No newline at end of file +Abort. diff --git a/test-suite/success/ProgramWf.v b/test-suite/success/ProgramWf.v index 681c4716b..85d7a770f 100644 --- a/test-suite/success/ProgramWf.v +++ b/test-suite/success/ProgramWf.v @@ -102,4 +102,4 @@ Qed. Program Fixpoint check_n' (n : nat) (m : {m:nat | m = n}) (p : nat) (q:{q : nat | q = p}) {measure (p - n) p} : nat := - _.
\ No newline at end of file + _. diff --git a/test-suite/success/cbn.v b/test-suite/success/cbn.v index 6aeb05f54..c98689c23 100644 --- a/test-suite/success/cbn.v +++ b/test-suite/success/cbn.v @@ -15,4 +15,4 @@ Goal forall n, foo (S n) = g n. match goal with |- g _ = g _ => reflexivity end. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/success/clear.v b/test-suite/success/clear.v index e25510cf0..03034cf13 100644 --- a/test-suite/success/clear.v +++ b/test-suite/success/clear.v @@ -30,4 +30,4 @@ Section Foo. assert(b:=Build_A). solve [ typeclasses eauto ]. Qed. -End Foo.
\ No newline at end of file +End Foo. diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v index b538d2ed2..9b11bc011 100644 --- a/test-suite/success/coercions.v +++ b/test-suite/success/coercions.v @@ -130,4 +130,4 @@ Local Coercion l2v2 : list >-> vect. of coercions *) Fail Check (fun l : list (T1 * T1) => (l : vect _ _)). Check (fun l : list (T1 * T1) => (l2v2 l : vect _ _)). -Section what_we_could_do.
\ No newline at end of file +Section what_we_could_do. diff --git a/test-suite/success/hintdb_in_ltac_bis.v b/test-suite/success/hintdb_in_ltac_bis.v index f5c25540e..2bc3f9d22 100644 --- a/test-suite/success/hintdb_in_ltac_bis.v +++ b/test-suite/success/hintdb_in_ltac_bis.v @@ -12,4 +12,4 @@ Goal Foo. progress foo mybase. Undo. progress bar mybase. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/success/indelim.v b/test-suite/success/indelim.v index 91b6dee2e..a962c29f4 100644 --- a/test-suite/success/indelim.v +++ b/test-suite/success/indelim.v @@ -58,4 +58,4 @@ Inductive color := Red | Black. Inductive option (A : Type) : Type := | None : option A -| Some : A -> option A.
\ No newline at end of file +| Some : A -> option A. diff --git a/test-suite/success/keyedrewrite.v b/test-suite/success/keyedrewrite.v index b88c142be..5638a7d3e 100644 --- a/test-suite/success/keyedrewrite.v +++ b/test-suite/success/keyedrewrite.v @@ -59,4 +59,4 @@ Qed. Lemma test b : b && true = b. Fail rewrite andb_true_l. Admitted. -
\ No newline at end of file + diff --git a/test-suite/success/ltac_match_pattern_names.v b/test-suite/success/ltac_match_pattern_names.v index 736329496..790cd1b3a 100644 --- a/test-suite/success/ltac_match_pattern_names.v +++ b/test-suite/success/ltac_match_pattern_names.v @@ -25,4 +25,4 @@ Ltac multiple_branches := let P := fresh P in let Q := fresh Q in idtac - end.
\ No newline at end of file + end. diff --git a/test-suite/success/ltac_plus.v b/test-suite/success/ltac_plus.v index 8a08d6465..01d477bdf 100644 --- a/test-suite/success/ltac_plus.v +++ b/test-suite/success/ltac_plus.v @@ -9,4 +9,4 @@ Proof. Fail ((apply h0+apply h2) || apply h1); apply h3. (* interaction with || *) ((apply h0+apply h1) || apply h2); apply h3. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/success/programequality.v b/test-suite/success/programequality.v index 414c572f8..05f4a7185 100644 --- a/test-suite/success/programequality.v +++ b/test-suite/success/programequality.v @@ -10,4 +10,4 @@ Proof. pi_eq_proofs. clear e. destruct e'. simpl. change (P a eq_refl). -Abort.
\ No newline at end of file +Abort. diff --git a/test-suite/success/rewrite_dep.v b/test-suite/success/rewrite_dep.v index d0aafd383..d73864e4e 100644 --- a/test-suite/success/rewrite_dep.v +++ b/test-suite/success/rewrite_dep.v @@ -31,4 +31,4 @@ Proof. intros. rewrite H0. reflexivity. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/success/rewrite_strat.v b/test-suite/success/rewrite_strat.v index 04c675563..a6e59fdda 100644 --- a/test-suite/success/rewrite_strat.v +++ b/test-suite/success/rewrite_strat.v @@ -50,4 +50,4 @@ Proof. Time Qed. (* 0.06 s *) Set Printing All. -Set Printing Depth 100000.
\ No newline at end of file +Set Printing Depth 100000. diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v index 269359ae6..fc74225d7 100644 --- a/test-suite/success/univers.v +++ b/test-suite/success/univers.v @@ -76,4 +76,4 @@ End Ind. Module Rec. Record box_in : myType := BoxIn { coord :> nat * nat; _ : is_box_in_shape coord }. -End Rec.
\ No newline at end of file +End Rec. diff --git a/test-suite/typeclasses/deftwice.v b/test-suite/typeclasses/deftwice.v index 439782c9e..139447702 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 663a837f3..518912433 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. diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v index 88cda79d8..247ea20a8 100644 --- a/theories/Arith/Peano_dec.v +++ b/theories/Arith/Peano_dec.v @@ -57,4 +57,4 @@ now rewrite H. Qed. (** For compatibility *) -Require Import Le Lt.
\ No newline at end of file +Require Import Le Lt. diff --git a/theories/FSets/FSets.v b/theories/FSets/FSets.v index 572f28654..e03fb2236 100644 --- a/theories/FSets/FSets.v +++ b/theories/FSets/FSets.v @@ -20,4 +20,4 @@ Require Export FSetEqProperties. Require Export FSetWeakList. Require Export FSetList. Require Export FSetPositive. -Require Export FSetAVL.
\ No newline at end of file +Require Export FSetAVL. diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v index 036ff1aa4..9fb8e499b 100644 --- a/theories/MSets/MSetGenTree.v +++ b/theories/MSets/MSetGenTree.v @@ -1144,4 +1144,4 @@ Proof. apply mindepth_cardinal. Qed. -End Props.
\ No newline at end of file +End Props. diff --git a/theories/MSets/MSets.v b/theories/MSets/MSets.v index f179bcd1d..1ee485cc1 100644 --- a/theories/MSets/MSets.v +++ b/theories/MSets/MSets.v @@ -18,4 +18,4 @@ Require Export MSetEqProperties. Require Export MSetWeakList. Require Export MSetList. Require Export MSetPositive. -Require Export MSetAVL.
\ No newline at end of file +Require Export MSetAVL. diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v index ba923d062..6771e57ad 100644 --- a/theories/NArith/BinNatDef.v +++ b/theories/NArith/BinNatDef.v @@ -378,4 +378,4 @@ Definition iter (n:N) {A} (f:A->A) (x:A) : A := | pos p => Pos.iter f x p end. -End N.
\ No newline at end of file +End N. diff --git a/theories/Numbers/NatInt/NZParity.v b/theories/Numbers/NatInt/NZParity.v index de3bbbca7..626d59d73 100644 --- a/theories/Numbers/NatInt/NZParity.v +++ b/theories/Numbers/NatInt/NZParity.v @@ -260,4 +260,4 @@ Proof. intros. apply odd_add_mul_even. apply even_spec, even_2. Qed. -End NZParityProp.
\ No newline at end of file +End NZParityProp. diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index 9aca56f47..b06562fc4 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -328,4 +328,4 @@ Ltac program_simpl := program_simplify ; try typeclasses eauto with program ; tr Obligation Tactic := program_simpl. -Definition obligation (A : Type) {a : A} := a.
\ No newline at end of file +Definition obligation (A : Type) {a : A} := a. diff --git a/theories/QArith/Qcabs.v b/theories/QArith/Qcabs.v index 1883c77be..09908665e 100644 --- a/theories/QArith/Qcabs.v +++ b/theories/QArith/Qcabs.v @@ -126,4 +126,4 @@ Proof. destruct (proj1 (Qcabs_Qcle_condition x 0)) as [A B]. + rewrite H; apply Qcle_refl. + apply Qcle_antisym; auto. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Ranalysis.v b/theories/Reals/Ranalysis.v index 66e37e867..9b0357f03 100644 --- a/theories/Reals/Ranalysis.v +++ b/theories/Reals/Ranalysis.v @@ -26,4 +26,4 @@ Require Export RList. Require Export Sqrt_reg. Require Export Ranalysis4. Require Export Rpower. -Require Export Ranalysis_reg.
\ No newline at end of file +Require Export Ranalysis_reg. diff --git a/theories/Vectors/Vector.v b/theories/Vectors/Vector.v index 672858fa5..19d749fc8 100644 --- a/theories/Vectors/Vector.v +++ b/theories/Vectors/Vector.v @@ -21,4 +21,4 @@ Require VectorSpec. Require VectorEq. Include VectorDef. Include VectorSpec. -Include VectorEq.
\ No newline at end of file +Include VectorEq. diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v index 7686fbae8..443667f48 100644 --- a/theories/ZArith/BinIntDef.v +++ b/theories/ZArith/BinIntDef.v @@ -616,4 +616,4 @@ Definition lxor a b := | neg a, neg b => of_N (N.lxor (Pos.pred_N a) (Pos.pred_N b)) end. -End Z.
\ No newline at end of file +End Z. diff --git a/theories/ZArith/Zsqrt_compat.v b/theories/ZArith/Zsqrt_compat.v index fb7f71b4b..cccd970da 100644 --- a/theories/ZArith/Zsqrt_compat.v +++ b/theories/ZArith/Zsqrt_compat.v @@ -229,4 +229,4 @@ Proof. symmetry. apply Z.sqrt_unique; trivial. now apply Zsqrt_interval. now destruct n. -Qed.
\ No newline at end of file +Qed. |