diff options
Diffstat (limited to 'test-suite/output')
39 files changed, 229 insertions, 107 deletions
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index 979396969a..d587d1f09b 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -42,32 +42,32 @@ Arguments D1, C1 are implicit and maximally inserted Argument scopes are [foo_scope type_scope _ _ _ _ _] The reduction tactics never unfold pf pf is transparent -Expands to: Constant Top.pf +Expands to: Constant Arguments.pf fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C Arguments A, B, C are implicit and maximally inserted Argument scopes are [type_scope type_scope type_scope _ _ _] The reduction tactics unfold fcomp when applied to 6 arguments fcomp is transparent -Expands to: Constant Top.fcomp +Expands to: Constant Arguments.fcomp volatile : nat -> nat Argument scope is [nat_scope] The reduction tactics always unfold volatile volatile is transparent -Expands to: Constant Top.volatile +Expands to: Constant Arguments.volatile f : T1 -> T2 -> nat -> unit -> nat -> nat Argument scopes are [_ _ nat_scope _ nat_scope] f is transparent -Expands to: Constant Top.S1.S2.f +Expands to: Constant Arguments.S1.S2.f f : T1 -> T2 -> nat -> unit -> nat -> nat Argument scopes are [_ _ nat_scope _ nat_scope] The reduction tactics unfold f when the 3rd, 4th and 5th arguments evaluate to a constructor f is transparent -Expands to: Constant Top.S1.S2.f +Expands to: Constant Arguments.S1.S2.f f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat Argument T2 is implicit @@ -75,7 +75,7 @@ Argument scopes are [type_scope _ _ nat_scope _ nat_scope] The reduction tactics unfold f when the 4th, 5th and 6th arguments evaluate to a constructor f is transparent -Expands to: Constant Top.S1.f +Expands to: Constant Arguments.S1.f f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat Arguments T1, T2 are implicit @@ -83,7 +83,7 @@ Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope] The reduction tactics unfold f when the 5th, 6th and 7th arguments evaluate to a constructor f is transparent -Expands to: Constant Top.f +Expands to: Constant Arguments.f = forall v : unit, f 0 0 5 v 3 = 2 : Prop = 2 = 2 @@ -93,7 +93,7 @@ f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat The reduction tactics unfold f when the 5th, 6th and 7th arguments evaluate to a constructor f is transparent -Expands to: Constant Top.f +Expands to: Constant Arguments.f forall w : r, w 3 true = tt : Prop The command has indeed failed with message: diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v index b67ac4f0df..97df40f882 100644 --- a/test-suite/output/Arguments.v +++ b/test-suite/output/Arguments.v @@ -1,3 +1,4 @@ +(* coq-prog-args: ("-top" "Arguments") *) Arguments Nat.sub n m : simpl nomatch. About Nat.sub. Arguments Nat.sub n / m : simpl nomatch. diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out index 6643c1429a..febe160820 100644 --- a/test-suite/output/ArgumentsScope.out +++ b/test-suite/output/ArgumentsScope.out @@ -10,12 +10,12 @@ negb'' : bool -> bool Argument scope is [bool_scope] negb'' is transparent -Expands to: Constant Top.A.B.negb'' +Expands to: Constant ArgumentsScope.A.B.negb'' negb' : bool -> bool Argument scope is [bool_scope] negb' is transparent -Expands to: Constant Top.A.negb' +Expands to: Constant ArgumentsScope.A.negb' negb : bool -> bool Argument scope is [bool_scope] @@ -34,11 +34,11 @@ Expands to: Constant Coq.Init.Datatypes.negb negb' : bool -> bool negb' is transparent -Expands to: Constant Top.A.negb' +Expands to: Constant ArgumentsScope.A.negb' negb'' : bool -> bool negb'' is transparent -Expands to: Constant Top.A.B.negb'' +Expands to: Constant ArgumentsScope.A.B.negb'' a : bool -> bool Expands to: Variable a @@ -49,8 +49,8 @@ Expands to: Constant Coq.Init.Datatypes.negb negb' : bool -> bool negb' is transparent -Expands to: Constant Top.negb' +Expands to: Constant ArgumentsScope.negb' negb'' : bool -> bool negb'' is transparent -Expands to: Constant Top.negb'' +Expands to: Constant ArgumentsScope.negb'' diff --git a/test-suite/output/ArgumentsScope.v b/test-suite/output/ArgumentsScope.v index 3a90cb79d7..ec49d85161 100644 --- a/test-suite/output/ArgumentsScope.v +++ b/test-suite/output/ArgumentsScope.v @@ -1,3 +1,4 @@ +(* coq-prog-args: ("-top" "ArgumentsScope") *) (* A few tests to check Global Argument Scope command *) Section A. diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index c0b04eb53f..1755886967 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -1,6 +1,6 @@ The command has indeed failed with message: Flag "rename" expected to rename A into B. -File "stdin", line 2, characters 0-25: +File "stdin", line 3, characters 0-25: Warning: This command is just asserting the names of arguments of identity. If this is what you want add ': assert' to silence the warning. If you want to clear implicit arguments add ': clear implicits'. If you want to clear @@ -41,7 +41,7 @@ myrefl : forall (B : Type) (x : A), B -> myEq B x x Arguments are renamed to C, x, _ Argument C is implicit and maximally inserted Argument scopes are [type_scope _ _] -Expands to: Constructor Top.Test1.myrefl +Expands to: Constructor Arguments_renaming.Test1.myrefl myplus = fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := match n with @@ -61,7 +61,7 @@ Argument scopes are [type_scope _ nat_scope nat_scope] The reduction tactics unfold myplus when the 2nd and 3rd arguments evaluate to a constructor myplus is transparent -Expands to: Constant Top.Test1.myplus +Expands to: Constant Arguments_renaming.Test1.myplus @myplus : forall Z : Type, Z -> nat -> nat -> nat Inductive myEq (A B : Type) (x : A) : A -> Prop := @@ -76,7 +76,7 @@ myrefl : forall (A B : Type) (x : A), B -> myEq A B x x Arguments are renamed to A, C, x, _ Argument C is implicit and maximally inserted Argument scopes are [type_scope type_scope _ _] -Expands to: Constructor Top.myrefl +Expands to: Constructor Arguments_renaming.myrefl myrefl : forall (A C : Type) (x : A), C -> myEq A C x x myplus = @@ -98,7 +98,7 @@ Argument scopes are [type_scope _ nat_scope nat_scope] The reduction tactics unfold myplus when the 2nd and 3rd arguments evaluate to a constructor myplus is transparent -Expands to: Constant Top.myplus +Expands to: Constant Arguments_renaming.myplus @myplus : forall Z : Type, Z -> nat -> nat -> nat The command has indeed failed with message: diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v index 0cb331347d..9713a9dbbe 100644 --- a/test-suite/output/Arguments_renaming.v +++ b/test-suite/output/Arguments_renaming.v @@ -1,3 +1,4 @@ +(* coq-prog-args: ("-top" "Arguments_renaming") *) Fail Arguments eq_refl {B y}, [B] y. Arguments identity A _ _. Arguments eq_refl A x : assert. diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index dfab400baa..cb835ab48d 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -64,14 +64,9 @@ In environment texpDenote : forall t : type, texp t -> typeDenote t t : type e : texp t -t1 : type -t2 : type -t0 : type -b : tbinop t1 t2 t0 -e1 : texp t1 -e2 : texp t2 -The term "0" has type "nat" while it is expected to have type - "typeDenote t0". +n : nat +The term "n" has type "nat" while it is expected to have type + "typeDenote ?t@{t1:=Nat}". fun '{{n, m, _}} => n + m : J -> nat fun '{{n, m, p}} => n + m + p diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index e4fa7044e7..43718a0f07 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -187,6 +187,7 @@ let p := fresh "p" in |- eq_refl ?p = _ => pose (match eq_refl p in _ = z return p=p /\ z=z with eq_refl => conj eq_refl eq_refl end) end. Show. +Abort. Set Printing Allow Match Default Clause. diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out index 24180c4553..cf2d5b2850 100644 --- a/test-suite/output/Errors.out +++ b/test-suite/output/Errors.out @@ -1,5 +1,5 @@ The command has indeed failed with message: -The field t is missing in Top.M. +The field t is missing in Errors.M. The command has indeed failed with message: Unable to unify "nat" with "True". The command has indeed failed with message: diff --git a/test-suite/output/Errors.v b/test-suite/output/Errors.v index c9b5091347..edc35f17b4 100644 --- a/test-suite/output/Errors.v +++ b/test-suite/output/Errors.v @@ -1,3 +1,4 @@ +(* coq-prog-args: ("-top" "Errors") *) (* Test error messages *) (* Test non-regression of bug fixed in r13486 (bad printer for module names) *) @@ -31,3 +32,6 @@ Abort. Fail Goal forall a f, f a = 0. Fail Goal forall f x, id f x = 0. Fail Goal forall f P, P (f 0). + +Definition t := unit. +End M. diff --git a/test-suite/output/Existentials.v b/test-suite/output/Existentials.v index 7388468399..924f1f5592 100644 --- a/test-suite/output/Existentials.v +++ b/test-suite/output/Existentials.v @@ -12,3 +12,5 @@ clearbody q. clear p. (* Error ... *) Show Existentials. +Abort. +End Test. diff --git a/test-suite/output/MExtraction.v b/test-suite/output/MExtraction.v index 352e422cf7..36992e4dda 100644 --- a/test-suite/output/MExtraction.v +++ b/test-suite/output/MExtraction.v @@ -7,6 +7,6 @@ Require Import QMicromega. Require Import RMicromega. Recursive Extraction - List.map RingMicromega.simpl_cone (*map_cone indexes*) - denorm Qpower vm_add - n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. + List.map simpl_cone (*map_cone indexes*) + denorm Qpower vm_add + normZ normQ normQ n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. diff --git a/test-suite/output/Match_subterm.v b/test-suite/output/Match_subterm.v index 2c44b1879f..bf862c946d 100644 --- a/test-suite/output/Match_subterm.v +++ b/test-suite/output/Match_subterm.v @@ -4,3 +4,4 @@ match goal with idtac v ; fail | _ => idtac 2 end. +Abort. diff --git a/test-suite/output/Nametab.out b/test-suite/output/Nametab.out index c11621d7c1..47b19b71b3 100644 --- a/test-suite/output/Nametab.out +++ b/test-suite/output/Nametab.out @@ -1,36 +1,39 @@ -Constant Top.Q.N.K.foo +Constant Nametab.Q.N.K.foo (shorter name to refer to it in current context is Q.N.K.foo) -Constant Top.Q.N.K.foo +Constant Nametab.Q.N.K.foo (shorter name to refer to it in current context is Q.N.K.foo) -Constant Top.Q.N.K.foo +Constant Nametab.Q.N.K.foo (shorter name to refer to it in current context is Q.N.K.foo) -Constant Top.Q.N.K.foo -Constant Top.Q.N.K.foo +Constant Nametab.Q.N.K.foo +Constant Nametab.Q.N.K.foo (shorter name to refer to it in current context is Q.N.K.foo) -Module Top.Q.N.K (shorter name to refer to it in current context is Q.N.K) -Module Top.Q.N.K (shorter name to refer to it in current context is Q.N.K) -Module Top.Q.N.K -Module Top.Q.N.K (shorter name to refer to it in current context is Q.N.K) -Module Top.Q.N (shorter name to refer to it in current context is Q.N) -Module Top.Q.N -Module Top.Q.N (shorter name to refer to it in current context is Q.N) -Module Top.Q -Module Top.Q (shorter name to refer to it in current context is Q) -Constant Top.Q.N.K.foo +Module Nametab.Q.N.K + (shorter name to refer to it in current context is Q.N.K) +Module Nametab.Q.N.K + (shorter name to refer to it in current context is Q.N.K) +Module Nametab.Q.N.K +Module Nametab.Q.N.K + (shorter name to refer to it in current context is Q.N.K) +Module Nametab.Q.N (shorter name to refer to it in current context is Q.N) +Module Nametab.Q.N +Module Nametab.Q.N (shorter name to refer to it in current context is Q.N) +Module Nametab.Q +Module Nametab.Q (shorter name to refer to it in current context is Q) +Constant Nametab.Q.N.K.foo (shorter name to refer to it in current context is K.foo) -Constant Top.Q.N.K.foo -Constant Top.Q.N.K.foo +Constant Nametab.Q.N.K.foo +Constant Nametab.Q.N.K.foo (shorter name to refer to it in current context is K.foo) -Constant Top.Q.N.K.foo +Constant Nametab.Q.N.K.foo (shorter name to refer to it in current context is K.foo) -Constant Top.Q.N.K.foo +Constant Nametab.Q.N.K.foo (shorter name to refer to it in current context is K.foo) -Module Top.Q.N.K -Module Top.Q.N.K (shorter name to refer to it in current context is K) -Module Top.Q.N.K (shorter name to refer to it in current context is K) -Module Top.Q.N.K (shorter name to refer to it in current context is K) -Module Top.Q.N (shorter name to refer to it in current context is Q.N) -Module Top.Q.N -Module Top.Q.N (shorter name to refer to it in current context is Q.N) -Module Top.Q -Module Top.Q (shorter name to refer to it in current context is Q) +Module Nametab.Q.N.K +Module Nametab.Q.N.K (shorter name to refer to it in current context is K) +Module Nametab.Q.N.K (shorter name to refer to it in current context is K) +Module Nametab.Q.N.K (shorter name to refer to it in current context is K) +Module Nametab.Q.N (shorter name to refer to it in current context is Q.N) +Module Nametab.Q.N +Module Nametab.Q.N (shorter name to refer to it in current context is Q.N) +Module Nametab.Q +Module Nametab.Q (shorter name to refer to it in current context is Q) diff --git a/test-suite/output/Nametab.v b/test-suite/output/Nametab.v index 357ba98243..4bbc5ca239 100644 --- a/test-suite/output/Nametab.v +++ b/test-suite/output/Nametab.v @@ -1,3 +1,4 @@ +(* coq-prog-args: ("-top" "Nametab") *) Module Q. Module N. Module K. @@ -10,19 +11,19 @@ End Q. (* Bad *) Locate K.foo. (* Bad *) Locate N.K.foo. (* OK *) Locate Q.N.K.foo. -(* OK *) Locate Top.Q.N.K.foo. +(* OK *) Locate Nametab.Q.N.K.foo. (* Bad *) Locate Module K. (* Bad *) Locate Module N.K. (* OK *) Locate Module Q.N.K. -(* OK *) Locate Module Top.Q.N.K. +(* OK *) Locate Module Nametab.Q.N.K. (* Bad *) Locate Module N. (* OK *) Locate Module Q.N. -(* OK *) Locate Module Top.Q.N. +(* OK *) Locate Module Nametab.Q.N. (* OK *) Locate Module Q. -(* OK *) Locate Module Top.Q. +(* OK *) Locate Module Nametab.Q. Import Q.N. @@ -32,16 +33,16 @@ Import Q.N. (* OK *) Locate K.foo. (* Bad *) Locate N.K.foo. (* OK *) Locate Q.N.K.foo. -(* OK *) Locate Top.Q.N.K.foo. +(* OK *) Locate Nametab.Q.N.K.foo. (* OK *) Locate Module K. (* Bad *) Locate Module N.K. (* OK *) Locate Module Q.N.K. -(* OK *) Locate Module Top.Q.N.K. +(* OK *) Locate Module Nametab.Q.N.K. (* Bad *) Locate Module N. (* OK *) Locate Module Q.N. -(* OK *) Locate Module Top.Q.N. +(* OK *) Locate Module Nametab.Q.N. (* OK *) Locate Module Q. -(* OK *) Locate Module Top.Q. +(* OK *) Locate Module Nametab.Q. diff --git a/test-suite/output/Naming.v b/test-suite/output/Naming.v index 327643dc57..7f3b332d7d 100644 --- a/test-suite/output/Naming.v +++ b/test-suite/output/Naming.v @@ -89,3 +89,4 @@ Show. apply H with (a:=a). (* test compliance with printing *) Abort. +End A. diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index cef7d1a702..46784d1897 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -1,5 +1,7 @@ [< 0 > + < 1 > * < 2 >] : nat +[< b > + < b > * < 2 >] + : nat [<< # 0 >>] : option nat [1 {f 1}] diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 9738ce5a5e..6bdbf1bed5 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -10,6 +10,10 @@ Notation "x * y" := (Nat.mul x y) (in custom myconstr at level 4). Notation "< x >" := x (in custom myconstr at level 3, x constr at level 10). Check [ < 0 > + < 1 > * < 2 >]. +Axiom a : nat. +Notation b := a. +Check [ < b > + < a > * < 2 >]. + Declare Custom Entry anotherconstr. Notation "[ x ]" := x (x custom myconstr at level 6). diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index 1307a8f26d..38a16e01c2 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -77,7 +77,7 @@ Expanded type for implicit arguments bar : forall x : nat, x = 0 Argument x is implicit and maximally inserted -Expands to: Constant Top.bar +Expands to: Constant PrintInfos.bar *** [ bar : foo ] Expanded type for implicit arguments @@ -85,8 +85,8 @@ bar : forall x : nat, x = 0 Argument x is implicit and maximally inserted Module Coq.Init.Peano -Notation existS2 := existT2 -Expands to: Notation Coq.Init.Specif.existS2 +Notation sym_eq := eq_sym +Expands to: Notation Coq.Init.Logic.sym_eq Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x For eq: Argument A is implicit and maximally inserted diff --git a/test-suite/output/PrintInfos.v b/test-suite/output/PrintInfos.v index a498db3e89..d7c271c3ec 100644 --- a/test-suite/output/PrintInfos.v +++ b/test-suite/output/PrintInfos.v @@ -1,3 +1,4 @@ +(* coq-prog-args: ("-top" "PrintInfos") *) About existT. Print existT. Print Implicit existT. @@ -26,8 +27,7 @@ About bar. Print bar. About Peano. (* Module *) -Set Warnings "-deprecated". -About existS2. (* Notation *) +About sym_eq. (* Notation *) Arguments eq_refl {A} {x}, {A} x. Print eq_refl. @@ -46,4 +46,3 @@ Goal forall n:nat, let g := newdef in n <> newdef n -> newdef n <> n -> False. About g. (* search hypothesis *) About h. (* search hypothesis *) Abort. - diff --git a/test-suite/output/PrintModule.out b/test-suite/output/PrintModule.out index 751d5fcc48..1a9bc068c5 100644 --- a/test-suite/output/PrintModule.out +++ b/test-suite/output/PrintModule.out @@ -1,5 +1,9 @@ Module N : S with Definition T := nat := M +Module N : S with Definition T := M + Module N : S with Module T := K := M +Module N : S with Module T := M + Module Type Func = Funsig (T0:Test) Sig Parameter x : T0.t. End diff --git a/test-suite/output/PrintModule.v b/test-suite/output/PrintModule.v index 5f30f7cda6..54ef305be4 100644 --- a/test-suite/output/PrintModule.v +++ b/test-suite/output/PrintModule.v @@ -1,3 +1,5 @@ +(* Bug #2169 *) + Module FOO. Module M. @@ -12,6 +14,10 @@ Module N : S with Definition T := nat := M. Print Module N. +Set Short Module Printing. +Print Module N. +Unset Short Module Printing. + End FOO. Module BAR. @@ -31,8 +37,14 @@ Module N : S with Module T := K := M. Print Module N. +Set Short Module Printing. +Print Module N. +Unset Short Module Printing. + End BAR. +(* Bug #4661 *) + Module QUX. Module Type Test. diff --git a/test-suite/output/RecordFieldErrors.out b/test-suite/output/RecordFieldErrors.out new file mode 100644 index 0000000000..5b67f632c9 --- /dev/null +++ b/test-suite/output/RecordFieldErrors.out @@ -0,0 +1,14 @@ +The command has indeed failed with message: +unit: Not a projection. +The command has indeed failed with message: +unit: Not a projection. +The command has indeed failed with message: +This record contains fields of both t and t'. +The command has indeed failed with message: +unit: Not a projection. +The command has indeed failed with message: +This record defines several times the field foo. +The command has indeed failed with message: +This record defines several times the field unit. +The command has indeed failed with message: +unit: Not a projection of inductive t. diff --git a/test-suite/output/RecordFieldErrors.v b/test-suite/output/RecordFieldErrors.v new file mode 100644 index 0000000000..27aa07822b --- /dev/null +++ b/test-suite/output/RecordFieldErrors.v @@ -0,0 +1,38 @@ +(** Check that various errors in record fields are reported with the correct +underlying issue. *) + +Record t := + { foo: unit }. + +Record t' := + { bar: unit }. + +Fail Check {| unit := tt |}. +(* unit: Not a projection. *) + +Fail Check {| unit := tt; + foo := tt |}. +(* unit: Not a projection. *) + +Fail Check {| foo := tt; + bar := tt |}. +(* This record contains fields of both t and t'. *) + +Fail Check {| unit := tt; + unit := tt |}. +(* unit: Not a projection. *) + +Fail Check {| foo := tt; + foo := tt |}. +(* This record defines several times the field foo. *) + +Fail Check {| foo := tt; + unit := tt; + unit := tt |}. +(* This is slightly wrong (would prefer "unit: Not a projection."), but it's +acceptable and seems an unlikely mistake. *) +(* This record defines several times the field unit. *) + +Fail Check {| foo := tt; + unit := tt |}. +(* unit: Not a projection of inductive t. *) diff --git a/test-suite/output/ShowMatch.v b/test-suite/output/ShowMatch.v index 02b7eada83..9cf6ad35b8 100644 --- a/test-suite/output/ShowMatch.v +++ b/test-suite/output/ShowMatch.v @@ -11,3 +11,4 @@ Module B. Inductive foo := f. (* local foo shadows A.foo, so constructor "f" needs disambiguation *) Show Match A.foo. +End B. diff --git a/test-suite/output/ShowProof.v b/test-suite/output/ShowProof.v index 73ecaf2200..19822ac50e 100644 --- a/test-suite/output/ShowProof.v +++ b/test-suite/output/ShowProof.v @@ -4,3 +4,4 @@ Proof. split. - exact I. Show Proof. (* Was not finding an evar name at some time *) +Abort. diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v index 75b66e463a..fa12f09a46 100644 --- a/test-suite/output/Tactics.v +++ b/test-suite/output/Tactics.v @@ -21,3 +21,4 @@ Proof. intros H. Fail intros [H%myid ?]. Fail destruct 1 as [H%myid ?]. +Abort. diff --git a/test-suite/output/TypeclassDebug.v b/test-suite/output/TypeclassDebug.v index d38e2a50e4..2e4008ae56 100644 --- a/test-suite/output/TypeclassDebug.v +++ b/test-suite/output/TypeclassDebug.v @@ -6,3 +6,4 @@ Hint Resolve H : foo. Goal foo. Typeclasses eauto := debug. Fail typeclasses eauto 5 with foo. +Abort. diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 926114a1e1..acc37f653c 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -5,7 +5,7 @@ PWrap has primitive projections with eta conversion. For PWrap: Argument scope is [type_scope] For pwrap: Argument scopes are [type_scope _] punwrap@{u} = -fun (A : Type@{u}) (p : PWrap@{u} A) => p.(punwrap) +fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p : forall A : Type@{u}, PWrap@{u} A -> A (* u |= *) @@ -42,10 +42,10 @@ bar@{u} = nat *) bar is universe polymorphic -foo@{u Top.17 v} = -Type@{Top.17} -> Type@{v} -> Type@{u} - : Type@{max(u+1,Top.17+1,v+1)} -(* u Top.17 v |= *) +foo@{u UnivBinders.17 v} = +Type@{UnivBinders.17} -> Type@{v} -> Type@{u} + : Type@{max(u+1,UnivBinders.17+1,v+1)} +(* u UnivBinders.17 v |= *) foo is universe polymorphic Type@{i} -> Type@{j} @@ -86,10 +86,10 @@ Type@{M} -> Type@{N} -> Type@{E} (* E M N |= *) foo is universe polymorphic -foo@{Top.16 Top.17 Top.18} = -Type@{Top.17} -> Type@{Top.18} -> Type@{Top.16} - : Type@{max(Top.16+1,Top.17+1,Top.18+1)} -(* Top.16 Top.17 Top.18 |= *) +foo@{u UnivBinders.17 v} = +Type@{UnivBinders.17} -> Type@{v} -> Type@{u} + : Type@{max(u+1,UnivBinders.17+1,v+1)} +(* u UnivBinders.17 v |= *) foo is universe polymorphic NonCumulative Inductive Empty@{E} : Type@{E} := @@ -104,7 +104,7 @@ punwrap@{K} : forall A : Type@{K}, PWrap@{K} A -> A punwrap is universe polymorphic Argument scopes are [type_scope _] punwrap is transparent -Expands to: Constant Top.punwrap +Expands to: Constant UnivBinders.punwrap The command has indeed failed with message: Universe instance should have length 3 The command has indeed failed with message: @@ -129,11 +129,19 @@ insec@{v} = Type@{u} -> Type@{v} (* v |= *) insec is universe polymorphic +NonCumulative Inductive insecind@{k} : Type@{k+1} := + inseccstr : Type@{k} -> insecind@{k} + +For inseccstr: Argument scope is [type_scope] insec@{u v} = Type@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* u v |= *) insec is universe polymorphic +NonCumulative Inductive insecind@{u k} : Type@{k+1} := + inseccstr : Type@{k} -> insecind@{u k} + +For inseccstr: Argument scope is [type_scope] inmod@{u} = Type@{u} : Type@{u+1} (* u |= *) @@ -155,27 +163,29 @@ inmod@{u} -> Type@{v} (* u v |= *) Applied.infunct is universe polymorphic -axfoo@{i Top.48 Top.49} : Type@{Top.48} -> Type@{i} -(* i Top.48 Top.49 |= *) +axfoo@{i UnivBinders.55 UnivBinders.56} : +Type@{UnivBinders.55} -> Type@{i} +(* i UnivBinders.55 UnivBinders.56 |= *) axfoo is universe polymorphic Argument scope is [type_scope] -Expands to: Constant Top.axfoo -axbar@{i Top.48 Top.49} : Type@{Top.49} -> Type@{i} -(* i Top.48 Top.49 |= *) +Expands to: Constant UnivBinders.axfoo +axbar@{i UnivBinders.55 UnivBinders.56} : +Type@{UnivBinders.56} -> Type@{i} +(* i UnivBinders.55 UnivBinders.56 |= *) axbar is universe polymorphic Argument scope is [type_scope] -Expands to: Constant Top.axbar -axfoo' : Type@{Top.51} -> Type@{axbar'.i} +Expands to: Constant UnivBinders.axbar +axfoo' : Type@{UnivBinders.58} -> Type@{axbar'.i} axfoo' is not universe polymorphic Argument scope is [type_scope] -Expands to: Constant Top.axfoo' -axbar' : Type@{Top.51} -> Type@{axbar'.i} +Expands to: Constant UnivBinders.axfoo' +axbar' : Type@{UnivBinders.58} -> Type@{axbar'.i} axbar' is not universe polymorphic Argument scope is [type_scope] -Expands to: Constant Top.axbar' +Expands to: Constant UnivBinders.axbar' The command has indeed failed with message: When declaring multiple axioms in one command, only the first is allowed a universe binder (which will be shared by the whole block). diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index f806a9f4f7..56474a0723 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -1,3 +1,4 @@ +(* coq-prog-args: ("-top" "UnivBinders") *) Set Universe Polymorphism. Set Printing Universes. (* Unset Strict Universe Declaration. *) @@ -58,7 +59,7 @@ Import mono. Check monomono. (* unqualified MONOU *) Check mono. (* still qualified mono.u *) -Monomorphic Constraint Set < Top.mono.u. +Monomorphic Constraint Set < UnivBinders.mono.u. Module mono2. Monomorphic Universe u. @@ -76,10 +77,10 @@ Module SecLet. Definition bobmorane := tt -> ff. End foo. Print bobmorane. (* - bobmorane@{Top.15 Top.16 ff.u ff.v} = - let tt := Type@{Top.16} in let ff := Type@{ff.v} in tt -> ff - : Type@{max(Top.15,ff.u)} - (* Top.15 Top.16 ff.u ff.v |= Top.16 < Top.15 + bobmorane@{UnivBinders.15 UnivBinders.16 ff.u ff.v} = + let tt := Type@{UnivBinders.16} in let ff := Type@{ff.v} in tt -> ff + : Type@{max(UnivBinders.15,ff.u)} + (* UnivBinders.15 UnivBinders.16 ff.u ff.v |= UnivBinders.16 < UnivBinders.15 ff.v < ff.u *) @@ -122,8 +123,12 @@ Section SomeSec. Universe u. Definition insec@{v} := Type@{u} -> Type@{v}. Print insec. + + Inductive insecind@{k} := inseccstr : Type@{k} -> insecind. + Print insecind. End SomeSec. Print insec. +Print insecind. Module SomeMod. Definition inmod@{u} := Type@{u}. diff --git a/test-suite/output/ltac_missing_args.out b/test-suite/output/ltac_missing_args.out index 7326f137c2..8a00cd3fe5 100644 --- a/test-suite/output/ltac_missing_args.out +++ b/test-suite/output/ltac_missing_args.out @@ -1,25 +1,25 @@ The command has indeed failed with message: -The user-defined tactic "Top.foo" was not fully applied: +The user-defined tactic "foo" was not fully applied: There is a missing argument for variable x, no arguments at all were provided. The command has indeed failed with message: -The user-defined tactic "Top.bar" was not fully applied: +The user-defined tactic "bar" was not fully applied: There is a missing argument for variable x, no arguments at all were provided. The command has indeed failed with message: -The user-defined tactic "Top.bar" was not fully applied: +The user-defined tactic "bar" was not fully applied: There are missing arguments for variables y and _, an argument was provided for variable x. The command has indeed failed with message: -The user-defined tactic "Top.baz" was not fully applied: +The user-defined tactic "baz" was not fully applied: There is a missing argument for variable x, no arguments at all were provided. The command has indeed failed with message: -The user-defined tactic "Top.qux" was not fully applied: +The user-defined tactic "qux" was not fully applied: There is a missing argument for variable x, no arguments at all were provided. The command has indeed failed with message: -The user-defined tactic "Top.mydo" was not fully applied: +The user-defined tactic "mydo" was not fully applied: There is a missing argument for variable _, no arguments at all were provided. The command has indeed failed with message: @@ -31,7 +31,7 @@ An unnamed user-defined tactic was not fully applied: There is a missing argument for variable _, no arguments at all were provided. The command has indeed failed with message: -The user-defined tactic "Top.rec" was not fully applied: +The user-defined tactic "rec" was not fully applied: There is a missing argument for variable x, no arguments at all were provided. The command has indeed failed with message: diff --git a/test-suite/output/names.v b/test-suite/output/names.v index f1efd0df2a..e9033bd732 100644 --- a/test-suite/output/names.v +++ b/test-suite/output/names.v @@ -7,3 +7,4 @@ Fail Definition b y : {x:nat|x=y} := a y. Goal (forall n m, n <= m -> m <= n -> n = m) -> True. intro H; epose proof (H _ 3) as H. Show. +Abort. diff --git a/test-suite/output/optimize_heap.v b/test-suite/output/optimize_heap.v index e566bd7bab..31b4510397 100644 --- a/test-suite/output/optimize_heap.v +++ b/test-suite/output/optimize_heap.v @@ -5,3 +5,4 @@ Goal True. Show. optimize_heap. Show. +Abort. diff --git a/test-suite/output/qualification.out b/test-suite/output/qualification.out index e9c70d1efc..cfa295010f 100644 --- a/test-suite/output/qualification.out +++ b/test-suite/output/qualification.out @@ -1,4 +1,5 @@ -File "stdin", line 19, characters 0-7: +File "stdin", line 20, characters 0-7: Error: Signature components for label test do not match: expected type -"Top.M2.t = Top.M2.M.t" but found type "Top.M2.t = Top.M2.t". +"qualification.M2.t = qualification.M2.M.t" but found type +"qualification.M2.t = qualification.M2.t". diff --git a/test-suite/output/qualification.v b/test-suite/output/qualification.v index d39097e2dd..877bc84d14 100644 --- a/test-suite/output/qualification.v +++ b/test-suite/output/qualification.v @@ -1,3 +1,4 @@ +(* coq-prog-args: ("-top" "qualification") *) Module Type T1. Parameter t : Type. End T1. diff --git a/test-suite/output/rewrite-2172.out b/test-suite/output/rewrite_2172.out index 27b0dc1b7b..27b0dc1b7b 100644 --- a/test-suite/output/rewrite-2172.out +++ b/test-suite/output/rewrite_2172.out diff --git a/test-suite/output/rewrite-2172.v b/test-suite/output/rewrite_2172.v index 212b1c1259..864fc21cdd 100644 --- a/test-suite/output/rewrite-2172.v +++ b/test-suite/output/rewrite_2172.v @@ -19,3 +19,4 @@ Proof. user in rewrite/induction/destruct calls). *) Fail rewrite <- axiom. +Abort. diff --git a/test-suite/output/unifconstraints.out b/test-suite/output/unifconstraints.out index ae84603622..2fadd747b7 100644 --- a/test-suite/output/unifconstraints.out +++ b/test-suite/output/unifconstraints.out @@ -63,3 +63,11 @@ unification constraint: True /\ True /\ True \/ veeryyyyyyyyyyyyloooooooooooooonggidentifier = veeryyyyyyyyyyyyloooooooooooooonggidentifier +The command has indeed failed with message: +In environment +P : nat -> Type +x : nat +h : P x +Unable to unify "P x" with "?P x" +(unable to find a well-typed instantiation for "?P": cannot ensure that +"nat -> Type" is a subtype of "nat -> Prop"). diff --git a/test-suite/output/unifconstraints.v b/test-suite/output/unifconstraints.v index b9413a4ac2..179dec3fb0 100644 --- a/test-suite/output/unifconstraints.v +++ b/test-suite/output/unifconstraints.v @@ -20,3 +20,9 @@ Goal forall n m : nat, True /\ True /\ True \/ 3:clear m. Show. Admitted. +Unset Printing Existential Instances. + +(* Check non regression of error message (the example can eventually + improve though and succeed) *) + +Fail Check fun P (x:nat) (h:P x) => exist _ x (h : P x). |