diff options
Diffstat (limited to 'test-suite')
88 files changed, 412 insertions, 173 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 3703d97c88..6696f1431e 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -1,7 +1,7 @@ ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## -## <O___,, # (see CREDITS file for the list of authors) ## +## v # Copyright INRIA, CNRS and contributors ## +## <O___,, # (see version control and CREDITS file for authors & dates) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## ## # GNU Lesser General Public License Version 2.1 ## diff --git a/test-suite/bugs/closed/bug_11811.v b/test-suite/bugs/closed/bug_11811.v new file mode 100644 index 0000000000..a73494b630 --- /dev/null +++ b/test-suite/bugs/closed/bug_11811.v @@ -0,0 +1,13 @@ + +Unset Positivity Checking. + +Inductive foo : Type -> Type := +| bar : foo (foo unit) +| baz : foo nat. + +Definition toto : forall A, foo A -> {A = foo unit} + {A = nat}. +Proof. + intros A x. destruct x; intuition. +Defined. + +Check (eq_refl : toto _ baz = right eq_refl). diff --git a/test-suite/bugs/closed/bug_11846.v b/test-suite/bugs/closed/bug_11846.v new file mode 100644 index 0000000000..53517e7703 --- /dev/null +++ b/test-suite/bugs/closed/bug_11846.v @@ -0,0 +1,16 @@ +Require Import FunInd. + +Inductive tree : Type := +| Node : unit -> tree. + +Definition height (s : tree) : unit := +match s with +| Node h => h +end. + +Definition bal : forall l, let h := height l in tree := fun l => + let h := height l in + Node h. + +Set Warnings "+all". +Functional Scheme bal_ind := Induction for bal Sort Prop. diff --git a/test-suite/bugs/closed/bug_9058.v b/test-suite/bugs/closed/bug_9058.v new file mode 100644 index 0000000000..6de8324641 --- /dev/null +++ b/test-suite/bugs/closed/bug_9058.v @@ -0,0 +1,16 @@ +Class A (X : Type) := {}. +Hint Mode A ! : typeclass_instances. + +Class B X {aX: A X} Y := { opB: X -> Y -> Y }. +Hint Mode B - - ! : typeclass_instances. + +Section Section. + +Context X {aX: A X} Y {bY: B X Y}. + +(* Set Typeclasses Debug. *) + +Let ok := fun (x : X) (y : Y) => opB x y. +Let ok' := fun x (y : Y) => opB x y. + +End Section. diff --git a/test-suite/failure/Tauto.v b/test-suite/failure/Tauto.v index 6eef3c9845..59c62bf641 100644 --- a/test-suite/failure/Tauto.v +++ b/test-suite/failure/Tauto.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/failure/clash_cons.v b/test-suite/failure/clash_cons.v index 88dee9a683..cbffb2aa9a 100644 --- a/test-suite/failure/clash_cons.v +++ b/test-suite/failure/clash_cons.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/failure/fixpoint1.v b/test-suite/failure/fixpoint1.v index 4b8e861616..4a09a0d7c7 100644 --- a/test-suite/failure/fixpoint1.v +++ b/test-suite/failure/fixpoint1.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/failure/guard.v b/test-suite/failure/guard.v index 023a494a66..b3883f8441 100644 --- a/test-suite/failure/guard.v +++ b/test-suite/failure/guard.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/failure/illtype1.v b/test-suite/failure/illtype1.v index 3988292248..a22c3a7183 100644 --- a/test-suite/failure/illtype1.v +++ b/test-suite/failure/illtype1.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/failure/positivity.v b/test-suite/failure/positivity.v index ec8eb35b87..72bc887ab7 100644 --- a/test-suite/failure/positivity.v +++ b/test-suite/failure/positivity.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/failure/redef.v b/test-suite/failure/redef.v index b1a578d15c..ef74815634 100644 --- a/test-suite/failure/redef.v +++ b/test-suite/failure/redef.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/failure/search.v b/test-suite/failure/search.v index 284acb88fc..4330cd82aa 100644 --- a/test-suite/failure/search.v +++ b/test-suite/failure/search.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ideal-features/Apply.v b/test-suite/ideal-features/Apply.v index 5e1218851a..a059f326b3 100644 --- a/test-suite/ideal-features/Apply.v +++ b/test-suite/ideal-features/Apply.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ltac2/binder.v b/test-suite/ltac2/binder.v new file mode 100644 index 0000000000..eac74688b2 --- /dev/null +++ b/test-suite/ltac2/binder.v @@ -0,0 +1,37 @@ +Require Import Ltac2.Ltac2. + +Ltac2 check () := +let t := Control.goal () in +match Constr.Unsafe.kind t with +| Constr.Unsafe.Prod b t => + let na := Constr.Binder.name b in + let u := Constr.Binder.type b in + let b := Constr.Binder.make na u in + let c := Constr.Unsafe.make (Constr.Unsafe.Prod b t) in + pose (v := $c); + refine '(_ : &v); + unfold &v +| _ => fail +end. + +Goal forall x : nat, x = x. +Proof. +check (); intros; reflexivity. +Qed. + +Goal forall x : Type, x = x. +Proof. +check (); intros; reflexivity. +Qed. + +Goal forall x : Set, x = x. +Proof. +check (); intros; reflexivity. +Qed. + +Inductive True : SProp := I. + +Goal forall x : True, True. +Proof. +check (); intros; constructor. +Qed. diff --git a/test-suite/ltac2/constr.v b/test-suite/ltac2/constr.v index 39601d99a8..018596ed95 100644 --- a/test-suite/ltac2/constr.v +++ b/test-suite/ltac2/constr.v @@ -2,11 +2,11 @@ Require Import Ltac2.Constr Ltac2.Init Ltac2.Control. Import Unsafe. Ltac2 Eval match (kind '(nat -> bool)) with - | Prod a b c => a + | Prod a c => a | _ => throw Match_failure end. Set Allow StrictProp. Axiom something : SProp. Ltac2 Eval match (kind '(forall x : something, bool)) with - | Prod a b c => a + | Prod a c => a | _ => throw Match_failure end. diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index f889da4e98..8cf0797b17 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -39,7 +39,7 @@ The reduction tactics unfold Nat.sub when the 1st and Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub pf : -forall D1 C1 : Type, +forall {D1 C1 : Type}, (D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2 pf is not universe polymorphic @@ -47,7 +47,7 @@ Arguments pf {D1}%foo_scope {C1}%type_scope _ [D2 C2] : simpl never The reduction tactics never unfold pf pf is transparent Expands to: Constant Arguments.pf -fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C +fcomp : forall {A B C : Type}, (B -> C) -> (A -> B) -> A -> C fcomp is not universe polymorphic Arguments fcomp {A B C}%type_scope _ _ _ / @@ -75,7 +75,7 @@ The reduction tactics unfold f when the 3rd, 4th and 5th arguments evaluate to a constructor f is transparent Expands to: Constant Arguments.S1.S2.f -f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat +f : forall [T2 : Type], T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic Arguments f [T2]%type_scope _ _ !_%nat_scope !_ !_%nat_scope @@ -83,7 +83,7 @@ The reduction tactics unfold f when the 4th, 5th and 6th arguments evaluate to a constructor f is transparent Expands to: Constant Arguments.S1.f -f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat +f : forall [T1 T2 : Type], T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic Arguments f [T1 T2]%type_scope _ _ !_%nat_scope !_ !_%nat_scope diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 26ebd8efc3..abc7f0f88e 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -15,7 +15,7 @@ Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x Arguments eq {A}%type_scope Arguments eq_refl {B}%type_scope {y}, [B] _ -eq_refl : forall (A : Type) (x : A), x = x +eq_refl : forall {A : Type} {x : A}, x = x eq_refl is not universe polymorphic Arguments eq_refl {B}%type_scope {y}, [B] _ @@ -24,7 +24,7 @@ Inductive myEq (B : Type) (x : A) : A -> Prop := myrefl : B -> myEq B x x Arguments myEq _%type_scope Arguments myrefl {C}%type_scope x : rename -myrefl : forall (B : Type) (x : A), B -> myEq B x x +myrefl : forall {B : Type} (x : A), B -> myEq B x x myrefl is not universe polymorphic Arguments myrefl {C}%type_scope x : rename @@ -38,7 +38,7 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := : forall T : Type, T -> nat -> nat -> nat Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename -myplus : forall T : Type, T -> nat -> nat -> nat +myplus : forall {T : Type}, T -> nat -> nat -> nat myplus is not universe polymorphic Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename @@ -53,7 +53,7 @@ Inductive myEq (A B : Type) (x : A) : A -> Prop := Arguments myEq (_ _)%type_scope Arguments myrefl A%type_scope {C}%type_scope x : rename -myrefl : forall (A B : Type) (x : A), B -> myEq A B x x +myrefl : forall (A : Type) {B : Type} (x : A), B -> myEq A B x x myrefl is not universe polymorphic Arguments myrefl A%type_scope {C}%type_scope x : rename @@ -69,7 +69,7 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := : forall T : Type, T -> nat -> nat -> nat Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename -myplus : forall T : Type, T -> nat -> nat -> nat +myplus : forall {T : Type}, T -> nat -> nat -> nat myplus is not universe polymorphic Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename diff --git a/test-suite/output/FloatExtraction.v b/test-suite/output/FloatExtraction.v index f296e8e871..7ff8958c0f 100644 --- a/test-suite/output/FloatExtraction.v +++ b/test-suite/output/FloatExtraction.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/output/MExtraction.v b/test-suite/output/MExtraction.v index 357afb51eb..22268daa83 100644 --- a/test-suite/output/MExtraction.v +++ b/test-suite/output/MExtraction.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/output/NoAxiomFromR.v b/test-suite/output/NoAxiomFromR.v index 9cf6879699..7abbe29452 100644 --- a/test-suite/output/NoAxiomFromR.v +++ b/test-suite/output/NoAxiomFromR.v @@ -5,6 +5,6 @@ Inductive TT : Set := Lemma lem4 : forall (n m : nat), S m <= m -> C (S m) <> C n -> False. -Proof. firstorder. Qed. +Proof. firstorder lia. Qed. Print Assumptions lem4. diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index 71d162c314..8fb267e343 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -1,4 +1,4 @@ -existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x} +existT : forall [A : Type] (P : A -> Type) (x : A), P x -> {x : A & P x} existT is template universe polymorphic on sigT.u0 sigT.u1 Arguments existT [A]%type_scope _%function_scope @@ -8,19 +8,19 @@ Inductive sigT (A : Type) (P : A -> Type) : Type := Arguments sigT [A]%type_scope _%type_scope Arguments existT [A]%type_scope _%function_scope -existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x} +existT : forall [A : Type] (P : A -> Type) (x : A), P x -> {x : A & P x} Argument A is implicit Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x Arguments eq {A}%type_scope Arguments eq_refl {A}%type_scope {x}, [A] _ -eq_refl : forall (A : Type) (x : A), x = x +eq_refl : forall {A : Type} {x : A}, x = x eq_refl is not universe polymorphic Arguments eq_refl {A}%type_scope {x}, [A] _ Expands to: Constructor Coq.Init.Logic.eq_refl -eq_refl : forall (A : Type) (x : A), x = x +eq_refl : forall {A : Type} {x : A}, x = x When applied to no arguments: Arguments A, x are implicit and maximally inserted @@ -65,14 +65,14 @@ bar : foo bar is not universe polymorphic Expanded type for implicit arguments -bar : forall x : nat, x = 0 +bar : forall {x : nat}, x = 0 Arguments bar {x} Expands to: Constant PrintInfos.bar *** [ bar : foo ] Expanded type for implicit arguments -bar : forall x : nat, x = 0 +bar : forall {x : nat}, x = 0 Arguments bar {x} Module Coq.Init.Peano diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index ffba1d35cc..9d8e830d64 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -18,6 +18,7 @@ le_sind: P n -> (forall m : nat, n <= m -> P m -> P (S m)) -> forall n0 : nat, n <= n0 -> P n0 +(use "About" for full details on implicit arguments) false: bool true: bool eq_true: bool -> Prop @@ -37,7 +38,7 @@ Nat.leb: nat -> nat -> bool Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b eq_true_ind_r: - forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true + forall (P : bool -> Prop) [b : bool], P b -> eq_true b -> P true eq_true_rec: forall P : bool -> Set, P true -> forall b : bool, eq_true b -> P b bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b @@ -49,9 +50,9 @@ bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b eq_true_ind: forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b eq_true_rec_r: - forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true + forall (P : bool -> Set) [b : bool], P b -> eq_true b -> P true eq_true_rect_r: - forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true + forall (P : bool -> Type) [b : bool], P b -> eq_true b -> P true bool_sind: forall P : bool -> SProp, P true -> P false -> forall b : bool, P b Byte.to_bits: @@ -62,13 +63,13 @@ Byte.of_bits: Byte.byte andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true andb_true_intro: - forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true + forall [b1 b2 : bool], b1 = true /\ b2 = true -> (b1 && b2)%bool = true BoolSpec_sind: - forall (P Q : Prop) (P0 : bool -> SProp), + forall [P Q : Prop] (P0 : bool -> SProp), (P -> P0 true) -> (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b BoolSpec_ind: - forall (P Q : Prop) (P0 : bool -> Prop), + forall [P Q : Prop] (P0 : bool -> Prop), (P -> P0 true) -> (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b Byte.to_bits_of_bits: @@ -76,9 +77,10 @@ Byte.to_bits_of_bits: b : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))), Byte.to_bits (Byte.of_bits b) = b bool_choice: - forall (S : Set) (R1 R2 : S -> Prop), + forall [S : Set] [R1 R2 : S -> Prop], (forall x : S, {R1 x} + {R2 x}) -> {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x} +(use "About" for full details on implicit arguments) mult_n_O: forall n : nat, 0 = n * 0 plus_O_n: forall n : nat, 0 + n = n plus_n_O: forall n : nat, n = n + 0 @@ -104,25 +106,35 @@ f_equal2_mult: f_equal2_nat: forall (B : Type) (f : nat -> nat -> B) (x1 y1 x2 y2 : nat), x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2 +(use "About" for full details on implicit arguments) andb_true_intro: - forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true + forall [b1 b2 : bool], b1 = true /\ b2 = true -> (b1 && b2)%bool = true andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true bool_choice: - forall (S : Set) (R1 R2 : S -> Prop), + forall [S : Set] [R1 R2 : S -> Prop], (forall x : S, {R1 x} + {R2 x}) -> {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x} +(use "About" for full details on implicit arguments) andb_true_intro: - forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true + forall [b1 b2 : bool], b1 = true /\ b2 = true -> (b1 && b2)%bool = true andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true +(use "About" for full details on implicit arguments) andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true +(use "About" for full details on implicit arguments) h: n <> newdef n h': newdef n <> n +(use "About" for full details on implicit arguments) h: n <> newdef n h': newdef n <> n +(use "About" for full details on implicit arguments) h: n <> newdef n +(use "About" for full details on implicit arguments) h: n <> newdef n +(use "About" for full details on implicit arguments) h: n <> newdef n h': newdef n <> n +(use "About" for full details on implicit arguments) +(use "About" for full details on implicit arguments) The command has indeed failed with message: No such goal. The command has indeed failed with message: @@ -131,9 +143,14 @@ The command has indeed failed with message: Query commands only support the single numbered goal selector. h: P n h': ~ P n +(use "About" for full details on implicit arguments) h: P n h': ~ P n +(use "About" for full details on implicit arguments) h: P n h': ~ P n +(use "About" for full details on implicit arguments) h: P n +(use "About" for full details on implicit arguments) h: P n +(use "About" for full details on implicit arguments) diff --git a/test-suite/output/SearchHead.out b/test-suite/output/SearchHead.out index 7038eac22c..5627e4bd3c 100644 --- a/test-suite/output/SearchHead.out +++ b/test-suite/output/SearchHead.out @@ -4,6 +4,7 @@ le_S: forall n m : nat, n <= m -> n <= S m le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m le_n_S: forall n m : nat, n <= m -> S n <= S m le_S_n: forall n m : nat, S n <= S m -> n <= m +(use "About" for full details on implicit arguments) false: bool true: bool negb: bool -> bool @@ -17,6 +18,7 @@ Nat.leb: nat -> nat -> bool Nat.ltb: nat -> nat -> bool Nat.testbit: nat -> nat -> bool Nat.eqb: nat -> nat -> bool +(use "About" for full details on implicit arguments) mult_n_O: forall n : nat, 0 = n * 0 plus_O_n: forall n : nat, 0 + n = n plus_n_O: forall n : nat, n = n + 0 @@ -35,5 +37,8 @@ f_equal2_plus: forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2 f_equal2_mult: forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2 +(use "About" for full details on implicit arguments) h: newdef n +(use "About" for full details on implicit arguments) h: P n +(use "About" for full details on implicit arguments) diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out index 4cd0ffb1dc..36fc1a5914 100644 --- a/test-suite/output/SearchPattern.out +++ b/test-suite/output/SearchPattern.out @@ -11,6 +11,7 @@ Nat.leb: nat -> nat -> bool Nat.ltb: nat -> nat -> bool Nat.testbit: nat -> nat -> bool Nat.eqb: nat -> nat -> bool +(use "About" for full details on implicit arguments) Nat.two: nat Nat.one: nat Nat.zero: nat @@ -44,8 +45,10 @@ Nat.tail_addmul: nat -> nat -> nat -> nat Nat.of_uint_acc: Decimal.uint -> nat -> nat Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat Nat.log2_iter: nat -> nat -> nat -> nat -> nat -length: forall A : Type, list A -> nat +length: forall [A : Type], list A -> nat Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat +(use "About" for full details on implicit arguments) +(use "About" for full details on implicit arguments) Nat.div2: nat -> nat Nat.sqrt: nat -> nat Nat.log2: nat -> nat @@ -74,18 +77,29 @@ Nat.of_uint_acc: Decimal.uint -> nat -> nat Nat.log2_iter: nat -> nat -> nat -> nat -> nat Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat +(use "About" for full details on implicit arguments) mult_n_Sm: forall n m : nat, n * m + n = n * S m +(use "About" for full details on implicit arguments) iff_refl: forall A : Prop, A <-> A le_n: forall n : nat, n <= n -identity_refl: forall (A : Type) (a : A), identity a a -eq_refl: forall (A : Type) (x : A), x = x +identity_refl: forall [A : Type] (a : A), identity a a +eq_refl: forall {A : Type} {x : A}, x = x Nat.divmod: nat -> nat -> nat -> nat -> nat * nat -conj: forall A B : Prop, A -> B -> A /\ B -pair: forall A B : Type, A -> B -> A * B +(use "About" for full details on implicit arguments) +conj: forall [A B : Prop], A -> B -> A /\ B +pair: forall {A B : Type}, A -> B -> A * B Nat.divmod: nat -> nat -> nat -> nat -> nat * nat +(use "About" for full details on implicit arguments) +(use "About" for full details on implicit arguments) h: n <> newdef n +(use "About" for full details on implicit arguments) h: n <> newdef n +(use "About" for full details on implicit arguments) h: P n +(use "About" for full details on implicit arguments) h': ~ P n +(use "About" for full details on implicit arguments) h: P n +(use "About" for full details on implicit arguments) h: P n +(use "About" for full details on implicit arguments) diff --git a/test-suite/output/SearchRewrite.out b/test-suite/output/SearchRewrite.out index 5edea5dff6..3c0880b20c 100644 --- a/test-suite/output/SearchRewrite.out +++ b/test-suite/output/SearchRewrite.out @@ -1,5 +1,10 @@ plus_n_O: forall n : nat, n = n + 0 +(use "About" for full details on implicit arguments) plus_O_n: forall n : nat, 0 + n = n +(use "About" for full details on implicit arguments) h: n = newdef n +(use "About" for full details on implicit arguments) h: n = newdef n +(use "About" for full details on implicit arguments) h: n = newdef n +(use "About" for full details on implicit arguments) diff --git a/test-suite/output/clear.out b/test-suite/output/clear.out new file mode 100644 index 0000000000..42e3abf26f --- /dev/null +++ b/test-suite/output/clear.out @@ -0,0 +1,5 @@ +1 subgoal + + z := 0 : nat + ============================ + True diff --git a/test-suite/output/clear.v b/test-suite/output/clear.v new file mode 100644 index 0000000000..d584cf752e --- /dev/null +++ b/test-suite/output/clear.v @@ -0,0 +1,8 @@ +Module Wish11692. + +(* Support for let-in in clear dependent *) + +Goal forall x : Prop, let z := 0 in let z' : (fun _ => True) x := I in let y := x in y -> True. +Proof. intros x z z' y H. clear dependent x. Show. exact I. Qed. + +End Wish11692. diff --git a/test-suite/output/ssr_explain_match.v b/test-suite/output/ssr_explain_match.v index 4a840fe20c..5c5a4e9e7b 100644 --- a/test-suite/output/ssr_explain_match.v +++ b/test-suite/output/ssr_explain_match.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/prerequisite/ssr_mini_mathcomp.v b/test-suite/prerequisite/ssr_mini_mathcomp.v index 048fb3b027..19524d5553 100644 --- a/test-suite/prerequisite/ssr_mini_mathcomp.v +++ b/test-suite/prerequisite/ssr_mini_mathcomp.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/prerequisite/ssr_ssrsyntax1.v b/test-suite/prerequisite/ssr_ssrsyntax1.v index 1ffc83ecf8..1882531b49 100644 --- a/test-suite/prerequisite/ssr_ssrsyntax1.v +++ b/test-suite/prerequisite/ssr_ssrsyntax1.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/absevarprop.v b/test-suite/ssr/absevarprop.v index d534443c32..37cd314ed5 100644 --- a/test-suite/ssr/absevarprop.v +++ b/test-suite/ssr/absevarprop.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/abstract_var2.v b/test-suite/ssr/abstract_var2.v index aaeb80646b..39c4eceb7c 100644 --- a/test-suite/ssr/abstract_var2.v +++ b/test-suite/ssr/abstract_var2.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/binders.v b/test-suite/ssr/binders.v index a4b77257dc..4c4925f9c0 100644 --- a/test-suite/ssr/binders.v +++ b/test-suite/ssr/binders.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/binders_of.v b/test-suite/ssr/binders_of.v index 3f60a480dc..c37a4820b4 100644 --- a/test-suite/ssr/binders_of.v +++ b/test-suite/ssr/binders_of.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/caseview.v b/test-suite/ssr/caseview.v index 098263ee4c..8da268b705 100644 --- a/test-suite/ssr/caseview.v +++ b/test-suite/ssr/caseview.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/congr.v b/test-suite/ssr/congr.v index f85791b00b..bb9eaa7dc1 100644 --- a/test-suite/ssr/congr.v +++ b/test-suite/ssr/congr.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/deferclear.v b/test-suite/ssr/deferclear.v index 817101a268..b45c90e99a 100644 --- a/test-suite/ssr/deferclear.v +++ b/test-suite/ssr/deferclear.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/dependent_type_err.v b/test-suite/ssr/dependent_type_err.v index 436813bc94..f72f5422b3 100644 --- a/test-suite/ssr/dependent_type_err.v +++ b/test-suite/ssr/dependent_type_err.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/derive_inversion.v b/test-suite/ssr/derive_inversion.v index a2c438f8fe..fd613f4451 100644 --- a/test-suite/ssr/derive_inversion.v +++ b/test-suite/ssr/derive_inversion.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/elim.v b/test-suite/ssr/elim.v index 15b1d91eef..31522dde19 100644 --- a/test-suite/ssr/elim.v +++ b/test-suite/ssr/elim.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/elim2.v b/test-suite/ssr/elim2.v index 52fc2ed333..a431b483d3 100644 --- a/test-suite/ssr/elim2.v +++ b/test-suite/ssr/elim2.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/elim_pattern.v b/test-suite/ssr/elim_pattern.v index ecc5d1d5c7..8fdbfae991 100644 --- a/test-suite/ssr/elim_pattern.v +++ b/test-suite/ssr/elim_pattern.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/first_n.v b/test-suite/ssr/first_n.v index 0d42a55390..42ba2e1da9 100644 --- a/test-suite/ssr/first_n.v +++ b/test-suite/ssr/first_n.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/gen_have.v b/test-suite/ssr/gen_have.v index 4adad3d3ac..ea130c1a2f 100644 --- a/test-suite/ssr/gen_have.v +++ b/test-suite/ssr/gen_have.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/gen_pattern.v b/test-suite/ssr/gen_pattern.v index 0120d77194..faf863ee6b 100644 --- a/test-suite/ssr/gen_pattern.v +++ b/test-suite/ssr/gen_pattern.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/have_TC.v b/test-suite/ssr/have_TC.v index c74282ed4f..9aac8dedf6 100644 --- a/test-suite/ssr/have_TC.v +++ b/test-suite/ssr/have_TC.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/have_transp.v b/test-suite/ssr/have_transp.v index d663780adc..7dd9c1b73f 100644 --- a/test-suite/ssr/have_transp.v +++ b/test-suite/ssr/have_transp.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/have_view_idiom.v b/test-suite/ssr/have_view_idiom.v index 623eaac2b9..a3aa6b4be6 100644 --- a/test-suite/ssr/have_view_idiom.v +++ b/test-suite/ssr/have_view_idiom.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/havesuff.v b/test-suite/ssr/havesuff.v index 3ca69bcc4c..b41eb5b423 100644 --- a/test-suite/ssr/havesuff.v +++ b/test-suite/ssr/havesuff.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/if_isnt.v b/test-suite/ssr/if_isnt.v index 23bc581213..b7d50d2015 100644 --- a/test-suite/ssr/if_isnt.v +++ b/test-suite/ssr/if_isnt.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/intro_beta.v b/test-suite/ssr/intro_beta.v index dce4650611..86d6d682db 100644 --- a/test-suite/ssr/intro_beta.v +++ b/test-suite/ssr/intro_beta.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/intro_noop.v b/test-suite/ssr/intro_noop.v index 9e141a9487..023f2bb892 100644 --- a/test-suite/ssr/intro_noop.v +++ b/test-suite/ssr/intro_noop.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/ipatalternation.v b/test-suite/ssr/ipatalternation.v index ae783ac7ed..1a87197637 100644 --- a/test-suite/ssr/ipatalternation.v +++ b/test-suite/ssr/ipatalternation.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/ltac_have.v b/test-suite/ssr/ltac_have.v index 3862aa72da..2e7761b669 100644 --- a/test-suite/ssr/ltac_have.v +++ b/test-suite/ssr/ltac_have.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/ltac_in.v b/test-suite/ssr/ltac_in.v index e379c21773..0303ee8ed9 100644 --- a/test-suite/ssr/ltac_in.v +++ b/test-suite/ssr/ltac_in.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/move_after.v b/test-suite/ssr/move_after.v index 45c23e30c3..d4d599ef10 100644 --- a/test-suite/ssr/move_after.v +++ b/test-suite/ssr/move_after.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/multiview.v b/test-suite/ssr/multiview.v index fcb7e2a520..d567f9b0a6 100644 --- a/test-suite/ssr/multiview.v +++ b/test-suite/ssr/multiview.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/occarrow.v b/test-suite/ssr/occarrow.v index 8d11219a23..e776176cce 100644 --- a/test-suite/ssr/occarrow.v +++ b/test-suite/ssr/occarrow.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/patnoX.v b/test-suite/ssr/patnoX.v index 2dea5fcb6d..ae8e8ce128 100644 --- a/test-suite/ssr/patnoX.v +++ b/test-suite/ssr/patnoX.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/pattern.v b/test-suite/ssr/pattern.v index ae4745b352..5e83186829 100644 --- a/test-suite/ssr/pattern.v +++ b/test-suite/ssr/pattern.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/primproj.v b/test-suite/ssr/primproj.v index 89aa56e8ec..0c585a970f 100644 --- a/test-suite/ssr/primproj.v +++ b/test-suite/ssr/primproj.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/rewpatterns.v b/test-suite/ssr/rewpatterns.v index 82d0112362..ff63c06c07 100644 --- a/test-suite/ssr/rewpatterns.v +++ b/test-suite/ssr/rewpatterns.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/set_lamda.v b/test-suite/ssr/set_lamda.v index a18dde31bf..428733863c 100644 --- a/test-suite/ssr/set_lamda.v +++ b/test-suite/ssr/set_lamda.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/set_pattern.v b/test-suite/ssr/set_pattern.v index b513673215..97beee40d6 100644 --- a/test-suite/ssr/set_pattern.v +++ b/test-suite/ssr/set_pattern.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/ssrsyntax2.v b/test-suite/ssr/ssrsyntax2.v index c98ab98742..5008c28fe8 100644 --- a/test-suite/ssr/ssrsyntax2.v +++ b/test-suite/ssr/ssrsyntax2.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/tc.v b/test-suite/ssr/tc.v index bffb20d39b..a0e5e54293 100644 --- a/test-suite/ssr/tc.v +++ b/test-suite/ssr/tc.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/typeof.v b/test-suite/ssr/typeof.v index bd51230157..5fdb825e49 100644 --- a/test-suite/ssr/typeof.v +++ b/test-suite/ssr/typeof.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/unfold_Opaque.v b/test-suite/ssr/unfold_Opaque.v index 0b220b31f5..c071a6dd0d 100644 --- a/test-suite/ssr/unfold_Opaque.v +++ b/test-suite/ssr/unfold_Opaque.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/unkeyed.v b/test-suite/ssr/unkeyed.v index eee1d1cf67..87bf1919c5 100644 --- a/test-suite/ssr/unkeyed.v +++ b/test-suite/ssr/unkeyed.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/view_case.v b/test-suite/ssr/view_case.v index d212d377b6..b1656e0fbc 100644 --- a/test-suite/ssr/view_case.v +++ b/test-suite/ssr/view_case.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/wlog_suff.v b/test-suite/ssr/wlog_suff.v index 3deceebb39..945985e863 100644 --- a/test-suite/ssr/wlog_suff.v +++ b/test-suite/ssr/wlog_suff.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/wlogletin.v b/test-suite/ssr/wlogletin.v index 2dca6d939f..e2dec0e651 100644 --- a/test-suite/ssr/wlogletin.v +++ b/test-suite/ssr/wlogletin.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ssr/wlong_intro.v b/test-suite/ssr/wlong_intro.v index c24b66f7b8..aa2a115fcd 100644 --- a/test-suite/ssr/wlong_intro.v +++ b/test-suite/ssr/wlong_intro.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v index 56a4fa0aad..df50aee507 100644 --- a/test-suite/success/Check.v +++ b/test-suite/success/Check.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/Field.v b/test-suite/success/Field.v index 31e442549b..3b2378c16b 100644 --- a/test-suite/success/Field.v +++ b/test-suite/success/Field.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/HintMode.v b/test-suite/success/HintMode.v new file mode 100644 index 0000000000..decddb73d1 --- /dev/null +++ b/test-suite/success/HintMode.v @@ -0,0 +1,20 @@ +Module Postponing. + +Class In A T := { IsIn : A -> T -> Prop }. +Class Empty T := { empty : T }. +Class EmptyIn (A T : Type) `{In A T} `{Empty T} := + { isempty : forall x, IsIn x empty -> False }. + +Hint Mode EmptyIn ! ! - - : typeclass_instances. +Hint Mode Empty ! : typeclass_instances. +Hint Mode In ! - : typeclass_instances. +Existing Class IsIn. +Goal forall A T `{In A T} `{Empty T} `{EmptyIn A T}, forall x : A, IsIn x empty -> False. + Proof. + intros. + eapply @isempty. (* Second goal needs to be solved first, to un-stuck the first one + (hence the Existing Class IsIn to allow finding the assumption of IsIn here) *) + all:typeclasses eauto. +Qed. + +End Postponing. diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v index ea0cf43451..15ee260910 100644 --- a/test-suite/success/Tauto.v +++ b/test-suite/success/Tauto.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v index 287c77c866..f5231ca0c0 100644 --- a/test-suite/success/TestRefine.v +++ b/test-suite/success/TestRefine.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index 3f96bf2c35..66305dfefa 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -1,3 +1,64 @@ +Module applydestruct. + Class Foo (A : Type) := + { bar : nat -> A; + baz : A -> nat }. + Hint Mode Foo + : typeclass_instances. + + Class C (A : Type). + Hint Mode C + : typeclass_instances. + + Variable fool : forall {A} {F : Foo A} (x : A), C A -> bar 0 = x. + (* apply leaves non-dependent subgoals of typeclass type + alone *) + Goal forall {A} {F : Foo A} (x : A), bar 0 = x. + Proof. + intros. apply fool. + match goal with + |[ |- C A ] => idtac + end. + Abort. + + Variable fooli : forall {A} {F : Foo A} {c : C A} (x : A), bar 0 = x. + (* apply tries to resolve implicit argument typeclass + constraints. *) + Goal forall {A} {F : Foo A} (x : A), bar 0 = x. + Proof. + intros. + Fail apply fooli. + Fail unshelve eapply fooli; solve [typeclasses eauto]. + eapply fooli. + Abort. + + (* It applies resolution after unification of the goal *) + Goal forall {A} {F : Foo A} {C : C A} (x : A), bar 0 = x. + Proof. + intros. apply fooli. + Abort. + Set Typeclasses Debug Verbosity 2. + + Inductive bazdestr {A} (F : Foo A) : nat -> Prop := + | isbas : bazdestr F 1. + + Variable fooinv : forall {A} {F : Foo A} (x : A), + bazdestr F (baz x). + + (* Destruct applies resolution early, before finding + occurrences to abstract. *) + Goal forall {A} {F : Foo A} {C : C A} (x : A), baz x = 0. + Proof. + intros. Fail destruct (fooinv _). + destruct (fooinv x). + Abort. + + Goal forall {A} {F : Foo A} (x y : A), x = y. + Proof. + intros. rewrite <- (fool x). rewrite <- (fool y). reflexivity. + match goal with + |[ |- C A ] => idtac + end. + Abort. +End applydestruct. + Module onlyclasses. (* In 8.6 we still allow non-class subgoals *) diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v index 28200f8783..cbe5b64039 100644 --- a/test-suite/success/eauto.v +++ b/test-suite/success/eauto.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/eqdecide.v b/test-suite/success/eqdecide.v index 17c6a93d21..f406f54b32 100644 --- a/test-suite/success/eqdecide.v +++ b/test-suite/success/eqdecide.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/export_hint.v b/test-suite/success/export_hint.v new file mode 100644 index 0000000000..e18f7c1bef --- /dev/null +++ b/test-suite/success/export_hint.v @@ -0,0 +1,22 @@ +Create HintDb foo. + +Module Foo. + +Axiom F : False. + +#[export] +Hint Immediate F : foo. + +End Foo. + +Goal False. +Proof. +Fail solve [auto with foo]. +Abort. + +Import Foo. + +Goal False. +Proof. +auto with foo. +Qed. diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v index 54c82ff6f1..7e65906dc2 100644 --- a/test-suite/success/extraction.v +++ b/test-suite/success/extraction.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/inds_type_sec.v b/test-suite/success/inds_type_sec.v index ed781b3a40..fcc238e89e 100644 --- a/test-suite/success/inds_type_sec.v +++ b/test-suite/success/inds_type_sec.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index c8e5be93e9..73fe53c757 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/mutual_ind.v b/test-suite/success/mutual_ind.v index ac734de9df..1050f004ed 100644 --- a/test-suite/success/mutual_ind.v +++ b/test-suite/success/mutual_ind.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v index b7ab75349e..7af09585d0 100644 --- a/test-suite/success/unfold.v +++ b/test-suite/success/unfold.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/typeclasses/NewSetoid.v b/test-suite/typeclasses/NewSetoid.v index c5238eff22..50e28322cb 100644 --- a/test-suite/typeclasses/NewSetoid.v +++ b/test-suite/typeclasses/NewSetoid.v @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |