diff options
Diffstat (limited to 'test-suite')
60 files changed, 584 insertions, 138 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 9d2277c37e..37091a49e5 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -36,9 +36,10 @@ include ../Makefile.common # easily overridden LIB := .. BIN := $(shell cd ..; pwd)/bin/ +COQFLAGS?= -coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -batch -test-mode -R prerequisite TestSuite -coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite +coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -batch -test-mode -R prerequisite TestSuite $(COQFLAGS) +coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite $(COQFLAGS) coqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite coqdoc := $(BIN)coqdoc coqtopbyte := $(BIN)coqtop.byte @@ -90,19 +91,17 @@ FAIL = >&2 echo 'FAILED $@' # Testing subsystems ####################################################################### -# Apart so that it can be easily skipped with overriding +# These targets can be skipped by doing `make TARGET= test-suite` COMPLEXITY := $(if $(bogomips),complexity) - BUGS := bugs/opened bugs/closed - INTERACTIVE := interactive - +UNIT_TESTS := unit-tests VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ output-modulo-time $(INTERACTIVE) micromega $(COMPLEXITY) modules stm \ coqdoc ssr # All subsystems -SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools unit-tests +SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools $(UNIT_TESTS) PREREQUISITELOG = prerequisite/admit.v.log \ prerequisite/make_local.v.log prerequisite/make_notation.v.log \ @@ -119,6 +118,10 @@ PREREQUISITELOG = prerequisite/admit.v.log \ all: run $(MAKE) report +# do nothing +.PHONY: noop +noop: ; + run: $(SUBSYSTEMS) bugs: $(BUGS) @@ -569,7 +572,7 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake)) @echo "TEST $<" $(HIDE){ \ echo $(call log_intro,$<); \ - $(BIN)fake_ide $< "-coqlib $(LIB) -boot -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off" 2>&1; \ + $(BIN)fake_ide $< "-coqlib $(LIB) -boot -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off $(call get_coq_prog_args,"$<")" 2>&1; \ if [ $$? = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ diff --git a/test-suite/bugs/opened/bug_4781.v b/test-suite/bugs/closed/bug_4781.v index 8b651ac22e..464a3de1b3 100644 --- a/test-suite/bugs/opened/bug_4781.v +++ b/test-suite/bugs/closed/bug_4781.v @@ -25,29 +25,29 @@ Goal True. let x := match constr:(Set) with ?y => constr:(y) end in pose x. (* This fails with an error: *) - Fail let term := constr:(I) in + let term := constr:(I) in let T := type of term in let x := constr:((_ : abstract_term term) : T) in let x := match constr:(x) with ?y => constr:(y) end in pose x. (* The command has indeed failed with message: Error: Variable y should be bound to a term. *) (* And the rest fail with Anomaly: Uncaught exception Not_found. Please report. *) - Fail let term := constr:(I) in + let term := constr:(I) in let T := type of term in let x := constr:((_ : abstract_term term) : T) in let x := match constr:(x) with ?y => y end in pose x. - Fail let term := constr:(I) in + let term := constr:(I) in let T := type of term in let x := constr:((_ : abstract_term term) : T) in let x := (eval cbv iota in x) in pose x. - Fail let term := constr:(I) in + let term := constr:(I) in let T := type of term in let x := constr:((_ : abstract_term term) : T) in let x := type of x in pose x. (* should succeed *) - Fail let term := constr:(I) in + let term := constr:(I) in let T := type of term in let x := constr:(_ : abstract_term term) in let x := type of x in @@ -70,7 +70,7 @@ Even stranger, consider:*) (*This works fine. But if I change the period to a semicolon, I get:*) - Fail let term := constr:(I) in + let term := constr:(I) in let T := type of term in let x := constr:((_ : abstract_term term) : T) in let y := (eval cbv iota in (let v : T := x in v)) in @@ -82,7 +82,7 @@ Even stranger, consider:*) (* should succeed *) (*and if I use the second one instead of [pose x] (note that using [idtac] works fine), I get:*) - Fail let term := constr:(I) in + let term := constr:(I) in let T := type of term in let x := constr:((_ : abstract_term term) : T) in let y := (eval cbv iota in (let v : T := x in v)) in @@ -92,3 +92,5 @@ Even stranger, consider:*) let x := (eval cbv delta [x'] in x') in let z := (eval cbv iota in x) in (* Error: Variable x should be bound to a term. *) idtac. (* should succeed *) + exact I. +Qed. diff --git a/test-suite/bugs/closed/bug_7904.v b/test-suite/bugs/closed/bug_7904.v new file mode 100644 index 0000000000..1e518e2adf --- /dev/null +++ b/test-suite/bugs/closed/bug_7904.v @@ -0,0 +1,13 @@ + + +Class abstract_term {T} (x : T) := by_abstract_term : T. +Hint Extern 0 (@abstract_term ?T ?x) => change T; abstract (exact x) : typeclass_instances. + +Goal True. + let term := constr:(I) in + let T := type of term in + let x := constr:((_ : abstract_term term) : T) in + let x := match constr:(x) with ?y => y end in + pose x as v. (* was Error: Variable x should be bound to a term but is bound to a constr. *) + exact v. +Qed. diff --git a/test-suite/bugs/closed/bug_8369.v b/test-suite/bugs/closed/bug_8369.v new file mode 100644 index 0000000000..9816954d0c --- /dev/null +++ b/test-suite/bugs/closed/bug_8369.v @@ -0,0 +1,3 @@ +(* Was failing in master with a not_found generated by the printer *) + +Fail Definition foo := fun '(u, v) p2 => (u, v). diff --git a/test-suite/bugs/closed/bug_8819.v b/test-suite/bugs/closed/bug_8819.v new file mode 100644 index 0000000000..a4cb9dcd14 --- /dev/null +++ b/test-suite/bugs/closed/bug_8819.v @@ -0,0 +1,2 @@ +Theorem foo (_ : nat) (H : bool) : bool. +Proof. exact H. Qed. diff --git a/test-suite/bugs/closed/bug_9229.v b/test-suite/bugs/closed/bug_9229.v new file mode 100644 index 0000000000..7514741af4 --- /dev/null +++ b/test-suite/bugs/closed/bug_9229.v @@ -0,0 +1,6 @@ +(* There was a problem of freshness with Infix choice of vars *) + +(* In particular, x and y were special... *) + +Infix "#" := (fun x y => x + y) (at level 50, left associativity). +Check (3 # 5). diff --git a/test-suite/bugs/closed/bug_9240.v b/test-suite/bugs/closed/bug_9240.v new file mode 100644 index 0000000000..e0901dc2d9 --- /dev/null +++ b/test-suite/bugs/closed/bug_9240.v @@ -0,0 +1,12 @@ +Register unit as core.IDProp.type. +Register tt as core.IDProp.idProp. + + +Inductive vec (A : Type) : nat -> Type := +| nil : vec A 0 +| cons : forall n : nat, A -> vec A n -> vec A (S n). + +Definition hd (A : Type) (n : nat) (v : vec A (S n)) : A := +match v in (vec _ (S n)) return A with +| cons _ _ h _ => h +end. (* assertion failure in evarconv *) diff --git a/test-suite/bugs/closed/bug_9300.v b/test-suite/bugs/closed/bug_9300.v new file mode 100644 index 0000000000..a80f3233a3 --- /dev/null +++ b/test-suite/bugs/closed/bug_9300.v @@ -0,0 +1,6 @@ +Existing Class True. + +Instance foo {n : nat} (x := I) : forall {b : bool} (s : nat * nat), True. auto. Defined. + +Fail Check foo (n := 3) true (s := (4 , 5)). +Check foo (n := 3) (b := true) (4 , 5). diff --git a/test-suite/bugs/opened/bug_3166.v b/test-suite/bugs/opened/bug_3166.v index e1c29a954c..baf87631f0 100644 --- a/test-suite/bugs/opened/bug_3166.v +++ b/test-suite/bugs/opened/bug_3166.v @@ -81,3 +81,4 @@ Goal forall T (x y : T) (p : x = y), True. compute in H0. change (fun (x' : T) (_ : y = x') => x' = y) with ((fun y => fun (x' : T) (_ : y = x') => x' = y) y) in H0. Fail pose proof (fun k => @eq_trans _ _ _ k H0). +Abort. diff --git a/test-suite/bugs/opened/bug_3754.v b/test-suite/bugs/opened/bug_3754.v index a717bbe735..18820b1a4c 100644 --- a/test-suite/bugs/opened/bug_3754.v +++ b/test-suite/bugs/opened/bug_3754.v @@ -282,3 +282,4 @@ Defined. rewrite <- ap_p_pp; rewrite_moveL_Mp_p. Set Debug Tactic Unification. Fail rewrite (concat_Ap ff2). + Abort. diff --git a/test-suite/bugs/opened/bug_3890.v b/test-suite/bugs/opened/bug_3890.v index 5c74addb62..78b2aa69b9 100644 --- a/test-suite/bugs/opened/bug_3890.v +++ b/test-suite/bugs/opened/bug_3890.v @@ -1,3 +1,5 @@ +Set Nested Proofs Allowed. + Class Foo. Class Bar := b : Type. diff --git a/test-suite/bugs/opened/bug_3938.v b/test-suite/bugs/opened/bug_3938.v index 2d0d1930f1..3c7c945ed8 100644 --- a/test-suite/bugs/opened/bug_3938.v +++ b/test-suite/bugs/opened/bug_3938.v @@ -4,3 +4,4 @@ Goal forall a b (f : nat -> Set), Nat.eq a b -> f a = f b. intros a b f H. rewrite H. (* Toplevel input, characters 15-25: Anomaly: Evar ?X11 was not declared. Please report. *) +Abort. diff --git a/test-suite/dune b/test-suite/dune index c5fa0bb14a..eae072553a 100644 --- a/test-suite/dune +++ b/test-suite/dune @@ -70,4 +70,4 @@ (progn ; XXX: we will allow to set the NJOBS variable in a future Dune ; version, either by using an env var or by letting Dune set `-j` - (run make -j 2 BIN= PRINT_LOGS=1)))) + (run make -j 2 BIN= PRINT_LOGS=1 UNIT_TESTS=%{env:COQ_UNIT_TEST=unit-tests})))) diff --git a/test-suite/ide/join-sync.fake b/test-suite/ide/join-sync.fake new file mode 100644 index 0000000000..236028ce46 --- /dev/null +++ b/test-suite/ide/join-sync.fake @@ -0,0 +1,20 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# Error resiliency + async proofs off +# coq-prog-args: ("-async-proofs" "off" "-async-proofs-command-error-resilience" "on") +# + +ADD { Lemma x : True. } +ADD { Proof using. } +ADD here { trivial. } +ADD { fail. } +ADD { Qed. } +ADD { Lemma y : True. } +ADD { Proof using. } +ADD { trivial. } +ADD { Qed. } +WAIT +FAILJOIN +ASSERT TIP here +ABORT diff --git a/test-suite/ide/join.fake b/test-suite/ide/join.fake new file mode 100644 index 0000000000..c4c696ad9a --- /dev/null +++ b/test-suite/ide/join.fake @@ -0,0 +1,20 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# Error resiliency +# + +ADD { Section x. } +ADD { Lemma x : True. } +ADD { Proof using. } +ADD here { trivial. } +ADD { fail. } +ADD { Qed. } +ADD { Lemma y : True. } +ADD { Proof using. } +ADD { trivial. } +ADD { Qed. } +ADD { End x. } +FAILJOIN +ASSERT TIP here +ABORT diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.v b/test-suite/output-modulo-time/ltacprof_cutoff.v index ae5d51bae8..b7c98aa134 100644 --- a/test-suite/output-modulo-time/ltacprof_cutoff.v +++ b/test-suite/output-modulo-time/ltacprof_cutoff.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-profile-ltac") -*- *) +(* -*- coq-prog-args: ("-async-proofs" "off" "-profile-ltac") -*- *) Require Coq.ZArith.BinInt. Module WithIdTac. Ltac sleep := do 50 (idtac; let sleep := (eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl) in idtac). diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index b071da86c9..583ea0cb43 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -11,7 +11,7 @@ eq_refl : ?y = ?y where ?y : [ |- nat] -Monomorphic Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x +Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x For eq_refl: Arguments are renamed to B, y For eq: Argument A is implicit and maximally inserted @@ -31,8 +31,7 @@ When applied to 1 argument: Argument B is implicit Argument scopes are [type_scope _] Expands to: Constructor Coq.Init.Logic.eq_refl -Monomorphic Inductive myEq (B : Type) (x : A) : A -> Prop := - myrefl : B -> myEq B x x +Inductive myEq (B : Type) (x : A) : A -> Prop := myrefl : B -> myEq B x x For myrefl: Arguments are renamed to C, x, _ For myrefl: Argument C is implicit and maximally inserted @@ -45,7 +44,7 @@ Arguments are renamed to C, x, _ Argument C is implicit and maximally inserted Argument scopes are [type_scope _ _] Expands to: Constructor Arguments_renaming.Test1.myrefl -Monomorphic myplus = +myplus = fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := match n with | 0 => m @@ -69,7 +68,7 @@ myplus is transparent Expands to: Constant Arguments_renaming.Test1.myplus @myplus : forall Z : Type, Z -> nat -> nat -> nat -Monomorphic Inductive myEq (A B : Type) (x : A) : A -> Prop := +Inductive myEq (A B : Type) (x : A) : A -> Prop := myrefl : B -> myEq A B x x For myrefl: Arguments are renamed to A, C, x, _ @@ -85,7 +84,7 @@ Argument scopes are [type_scope type_scope _ _] Expands to: Constructor Arguments_renaming.myrefl myrefl : forall (A C : Type) (x : A), C -> myEq A C x x -Monomorphic myplus = +myplus = fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := match n with | 0 => m diff --git a/test-suite/output/Binder.out b/test-suite/output/Binder.out index 9c46ace463..6e27837b26 100644 --- a/test-suite/output/Binder.out +++ b/test-suite/output/Binder.out @@ -1,10 +1,10 @@ -Monomorphic foo = fun '(x, y) => x + y +foo = fun '(x, y) => x + y : nat * nat -> nat foo is not universe polymorphic forall '(a, b), a /\ b : Prop -Monomorphic foo = λ '(x, y), x + y +foo = λ '(x, y), x + y : nat * nat → nat foo is not universe polymorphic diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 0a02c5a7dd..efcc299e82 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -1,4 +1,4 @@ -Monomorphic t_rect = +t_rect = fun (P : t -> Type) (f : let x := t in forall x0 : x, P x0 -> P (k x0)) => fix F (t : t) : P t := match t as t0 return (P t0) with @@ -17,7 +17,7 @@ Argument scopes are [function_scope function_scope _] | {| f3 := b |} => b end : TT -> 0 = 0 -Monomorphic proj = +proj = fun (x y : nat) (P : nat -> Type) (def : P x) (prf : P y) => match Nat.eq_dec x y with | left eqprf => match eqprf in (_ = z) return (P z) with @@ -29,7 +29,7 @@ end proj is not universe polymorphic Argument scopes are [nat_scope nat_scope function_scope _ _] -Monomorphic foo = +foo = fix foo (A : Type) (l : list A) {struct l} : option A := match l with | nil => None @@ -40,7 +40,7 @@ fix foo (A : Type) (l : list A) {struct l} : option A := foo is not universe polymorphic Argument scopes are [type_scope list_scope] -Monomorphic uncast = +uncast = fun (A : Type) (x : I A) => match x with | x0 <: _ => x0 end @@ -48,11 +48,11 @@ fun (A : Type) (x : I A) => match x with uncast is not universe polymorphic Argument scopes are [type_scope _] -Monomorphic foo' = if A 0 then true else false +foo' = if A 0 then true else false : bool foo' is not universe polymorphic -Monomorphic f = +f = fun H : B => match H with | AC x => @@ -83,18 +83,18 @@ fun '(D n m p q) => n + m + p + q : J -> nat The command has indeed failed with message: The constructor D (in type J) expects 3 arguments. -Monomorphic lem1 = +lem1 = fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl : forall k : nat * nat, k = k lem1 is not universe polymorphic -Monomorphic lem2 = +lem2 = fun dd : bool => if dd as aa return (aa = aa) then eq_refl else eq_refl : forall k : bool, k = k lem2 is not universe polymorphic Argument scope is [bool_scope] -Monomorphic lem3 = +lem3 = fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl : forall k : nat * nat, k = k diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 43718a0f07..4e949dcb04 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -43,6 +43,7 @@ Print foo. (* Accept and use notation with binded parameters *) +#[universes(template)] Inductive I (A: Type) : Type := C : A -> I A. Notation "x <: T" := (C T x) (at level 38). @@ -83,6 +84,7 @@ Print f. (* Was enhancement request #5142 (error message reported on the most general return clause heuristic) *) +#[universes(template)] Inductive gadt : Type -> Type := | gadtNat : nat -> gadt nat | gadtTy : forall T, T -> gadt T. diff --git a/test-suite/output/Coercions.v b/test-suite/output/Coercions.v index 0e84bf3966..6976f35a88 100644 --- a/test-suite/output/Coercions.v +++ b/test-suite/output/Coercions.v @@ -1,7 +1,7 @@ (* Submitted by Randy Pollack *) -Record pred (S : Set) : Type := {sp_pred :> S -> Prop}. -Record rel (S : Set) : Type := {sr_rel :> S -> S -> Prop}. +#[universes(template)] Record pred (S : Set) : Type := {sp_pred :> S -> Prop}. +#[universes(template)] Record rel (S : Set) : Type := {sr_rel :> S -> S -> Prop}. Section testSection. Variables (S : Set) (P : pred S) (R : rel S) (x : S). diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out index cf2d5b2850..14c48e8fa0 100644 --- a/test-suite/output/Errors.out +++ b/test-suite/output/Errors.out @@ -9,10 +9,11 @@ The command has indeed failed with message: Ltac call to "instantiate ( (ident) := (lglob) )" failed. Instance is not well-typed in the environment of ?x. The command has indeed failed with message: -Cannot infer the domain of the type of f. +Cannot infer ?T in the partial instance "?T -> nat" found for the type of f. The command has indeed failed with message: -Cannot infer the domain of the implicit parameter A of id whose type is -"Type". +Cannot infer ?T in the partial instance "?T -> nat" found for the implicit +parameter A of id whose type is "Type". The command has indeed failed with message: -Cannot infer the codomain of the type of f in environment: +Cannot infer ?T in the partial instance "forall x : nat, ?T" found for the +type of f in environment: x : nat diff --git a/test-suite/output/Extraction_matchs_2413.v b/test-suite/output/Extraction_matchs_2413.v index 1ecd9771eb..f9398fdca9 100644 --- a/test-suite/output/Extraction_matchs_2413.v +++ b/test-suite/output/Extraction_matchs_2413.v @@ -101,7 +101,7 @@ Section decoder_result. Variable inst : Type. - Inductive decoder_result : Type := + #[universes(template)] Inductive decoder_result : Type := | DecUndefined : decoder_result | DecUnpredictable : decoder_result | DecInst : inst -> decoder_result diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v index 61ae4edbd1..9b25c2dbd3 100644 --- a/test-suite/output/Fixpoint.v +++ b/test-suite/output/Fixpoint.v @@ -44,7 +44,7 @@ fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1). omega. Qed. -CoInductive Inf := S { projS : Inf }. +#[universes(template)] CoInductive Inf := S { projS : Inf }. Definition expand_Inf (x : Inf) := S (projS x). CoFixpoint inf := S inf. Eval compute in inf. diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out index 71c7070f2b..0b0f501f9a 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -2,8 +2,7 @@ compose (C:=nat) S : (nat -> nat) -> nat -> nat ex_intro (P:=fun _ : nat => True) (x:=0) I : ex (fun _ : nat => True) -Monomorphic d2 = -fun x : nat => d1 (y:=x) +d2 = fun x : nat => d1 (y:=x) : forall x x0 : nat, x0 = x -> x0 = x d2 is not universe polymorphic diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out index 5a548cfae4..2ba02924c9 100644 --- a/test-suite/output/Inductive.out +++ b/test-suite/output/Inductive.out @@ -1,8 +1,7 @@ The command has indeed failed with message: Last occurrence of "list'" must have "A" as 1st argument in "A -> list' A -> list' (A * A)". -Monomorphic Inductive foo (A : Type) (x : A) (y : A := x) : Prop := - Foo : foo A x +Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x For foo: Argument scopes are [type_scope _] For Foo: Argument scopes are [type_scope _] diff --git a/test-suite/output/Inductive.v b/test-suite/output/Inductive.v index 8ff91268a6..9eec9a7dad 100644 --- a/test-suite/output/Inductive.v +++ b/test-suite/output/Inductive.v @@ -3,5 +3,5 @@ Fail Inductive list' (A:Set) : Set := | cons' : A -> list' A -> list' (A*A). (* Check printing of let-ins *) -Inductive foo (A : Type) (x : A) (y := x) := Foo. +#[universes(template)] Inductive foo (A : Type) (x : A) (y := x) := Foo. Print foo. diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out index 4743fb0d0a..c17c63e724 100644 --- a/test-suite/output/InitSyntax.out +++ b/test-suite/output/InitSyntax.out @@ -1,4 +1,4 @@ -Monomorphic Inductive sig2 (A : Type) (P Q : A -> Prop) : Type := +Inductive sig2 (A : Type) (P Q : A -> Prop) : Type := exist2 : forall x : A, P x -> Q x -> {x : A | P x & Q x} For sig2: Argument A is implicit diff --git a/test-suite/output/Load.out b/test-suite/output/Load.out index f84cedfa62..ebbd5d422b 100644 --- a/test-suite/output/Load.out +++ b/test-suite/output/Load.out @@ -1,8 +1,8 @@ -Monomorphic f = 2 +f = 2 : nat f is not universe polymorphic -Monomorphic u = I +u = I : True u is not universe polymorphic diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index f53313def9..71d92482d0 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -225,7 +225,7 @@ fun S : nat => [[S | S + S]] : Set exists2 '{{y, z}} : nat * nat, y > z & z > y : Prop -Monomorphic foo = +foo = fun l : list nat => match l with | _ :: (_ :: _) as l1 => l1 | _ => l @@ -261,11 +261,11 @@ myfoo01 tt {4; 5; 6}; {7; 8; 9}] : list (list nat) -Monomorphic amatch = mmatch 0 (with 0 => 1| 1 => 2 end) +amatch = mmatch 0 (with 0 => 1| 1 => 2 end) : unit amatch is not universe polymorphic -Monomorphic alist = [0; 1; 2] +alist = [0; 1; 2] : list nat alist is not universe polymorphic diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 15211f1233..2caffad1d9 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -123,7 +123,7 @@ Check fun n => foo4 n (fun x y z => (fun _ => y=0) z). (**********************************************************************) (* Test printing of #4932 *) -Inductive ftele : Type := +#[universes(template)] Inductive ftele : Type := | fb {T:Type} : T -> ftele | fr {T} : (T -> ftele) -> ftele. diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index d58e4bf2d6..94016e170b 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -45,3 +45,5 @@ fun x : nat => (x.-1)%pred : Prop ## : Prop +Notation Cn := Foo.FooCn +Expands to: Notation Top.J.Mfoo.Foo.Bar.Cn diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 61206b6dd0..309115848f 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -164,3 +164,20 @@ Open Scope my_scope. Check ##. End H. + +(* Fixing a bug reported by G. Gonthier in #9207 *) + +Module J. + +Module Import Mfoo. +Module Foo. +Definition FooCn := 2. +Module Bar. +Notation Cn := FooCn. +End Bar. +End Foo. +Export Foo.Bar. +End Mfoo. +About Cn. + +End J. diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out index bfeff20524..bdbc5a5960 100644 --- a/test-suite/output/PatternsInBinders.out +++ b/test-suite/output/PatternsInBinders.out @@ -1,4 +1,4 @@ -Monomorphic swap = fun '(x, y) => (y, x) +swap = fun '(x, y) => (y, x) : A * B -> B * A swap is not universe polymorphic @@ -6,22 +6,20 @@ fun '(x, y) => (y, x) : A * B -> B * A forall '(x, y), swap (x, y) = (y, x) : Prop -Monomorphic proj_informative = -fun '(exist _ x _) => x : A +proj_informative = fun '(exist _ x _) => x : A : {x : A | P x} -> A proj_informative is not universe polymorphic -Monomorphic foo = -fun '(Bar n b tt p) => if b then n + p else n - p +foo = fun '(Bar n b tt p) => if b then n + p else n - p : Foo -> nat foo is not universe polymorphic -Monomorphic baz = +baz = fun '(Bar n1 _ tt p1) '(Bar _ _ tt _) => n1 + p1 : Foo -> Foo -> nat baz is not universe polymorphic -Monomorphic swap = +swap = fun (A B : Type) '(x, y) => (y, x) : forall A B : Type, A * B -> B * A @@ -40,7 +38,7 @@ exists '(x, y) '(z, w), swap (x, y) = (z, w) : A * B → B * A ∀ '(x, y), swap (x, y) = (y, x) : Prop -Monomorphic both_z = +both_z = fun pat : nat * nat => let '(n, p) as x := pat return (F x) in (Z n, Z p) : F (n, p) : forall pat : nat * nat, F pat @@ -52,7 +50,7 @@ forall '(x, y) '(z, t), swap (x, y) = (z, t) : Prop fun (pat : nat) '(x, y) => x + y = pat : nat -> nat * nat -> Prop -Monomorphic f = fun x : nat => x + x +f = fun x : nat => x + x : nat -> nat f is not universe polymorphic diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v index d671053c07..0c1b08f5a3 100644 --- a/test-suite/output/PatternsInBinders.v +++ b/test-suite/output/PatternsInBinders.v @@ -53,7 +53,7 @@ Module Suboptimal. (** This test shows an example which exposes the [let] introduced by the pattern notation in binders. *) -Inductive Fin (n:nat) := Z : Fin n. +#[universes(template)] Inductive Fin (n:nat) := Z : Fin n. Definition F '(n,p) : Type := (Fin n * Fin p)%type. Definition both_z '(n,p) : F (n,p) := (Z _,Z _). Print both_z. diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index be793dd453..da1fca7134 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -4,7 +4,7 @@ existT is template universe polymorphic Argument A is implicit Argument scopes are [type_scope function_scope _ _] Expands to: Constructor Coq.Init.Specif.existT -Monomorphic Inductive sigT (A : Type) (P : A -> Type) : Type := +Inductive sigT (A : Type) (P : A -> Type) : Type := existT : forall x : A, P x -> {x : A & P x} For sigT: Argument A is implicit @@ -14,7 +14,7 @@ For existT: Argument scopes are [type_scope function_scope _ _] existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x} Argument A is implicit -Monomorphic Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x +Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x For eq: Argument A is implicit and maximally inserted For eq_refl, when applied to no arguments: @@ -38,7 +38,7 @@ When applied to no arguments: Arguments A, x are implicit and maximally inserted When applied to 1 argument: Argument A is implicit -Monomorphic Nat.add = +Nat.add = fix add (n m : nat) {struct n} : nat := match n with | 0 => m @@ -62,7 +62,7 @@ plus_n_O is not universe polymorphic Argument scope is [nat_scope] plus_n_O is opaque Expands to: Constant Coq.Init.Peano.plus_n_O -Monomorphic Inductive le (n : nat) : nat -> Prop := +Inductive le (n : nat) : nat -> Prop := le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m For le_S: Argument m is implicit @@ -74,7 +74,7 @@ comparison : Set comparison is not universe polymorphic Expands to: Inductive Coq.Init.Datatypes.comparison -Monomorphic Inductive comparison : Set := +Inductive comparison : Set := Eq : comparison | Lt : comparison | Gt : comparison bar : foo @@ -84,7 +84,7 @@ bar : forall x : nat, x = 0 Argument x is implicit and maximally inserted Expands to: Constant PrintInfos.bar -Monomorphic *** [ bar : foo ] +*** [ bar : foo ] bar is not universe polymorphic Expanded type for implicit arguments @@ -94,7 +94,7 @@ Argument x is implicit and maximally inserted Module Coq.Init.Peano Notation sym_eq := eq_sym Expands to: Notation Coq.Init.Logic.sym_eq -Monomorphic Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x +Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x For eq: Argument A is implicit and maximally inserted For eq_refl, when applied to no arguments: diff --git a/test-suite/output/Projections.v b/test-suite/output/Projections.v index 098a518dc4..2713e6a188 100644 --- a/test-suite/output/Projections.v +++ b/test-suite/output/Projections.v @@ -5,7 +5,7 @@ Class HostFunction := host_func : Type. Section store. Context `{HostFunction}. - Record store := { store_funcs : host_func }. + #[universes(template)] Record store := { store_funcs : host_func }. End store. Check (fun (S:@store nat) => S.(store_funcs)). diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v index d9a649fadc..4fe7b051f8 100644 --- a/test-suite/output/Record.v +++ b/test-suite/output/Record.v @@ -20,12 +20,12 @@ Check {| field := 5 |}. Check build_r 5. Check build_c 5. -Record N := C { T : Type; _ : True }. +#[universes(template)] Record N := C { T : Type; _ : True }. Check fun x:N => let 'C _ p := x in p. Check fun x:N => let 'C T _ := x in T. Check fun x:N => let 'C T p := x in (T,p). -Record M := D { U : Type; a := 0; q : True }. +#[universes(template)] Record M := D { U : Type; a := 0; q : True }. Check fun x:M => let 'D T _ p := x in p. Check fun x:M => let 'D T _ p := x in T. Check fun x:M => let 'D T p := x in (T,p). diff --git a/test-suite/output/ShowMatch.v b/test-suite/output/ShowMatch.v index 9cf6ad35b8..99183f2064 100644 --- a/test-suite/output/ShowMatch.v +++ b/test-suite/output/ShowMatch.v @@ -3,12 +3,12 @@ *) Module A. - Inductive foo := f. + #[universes(template)] Inductive foo := f. Show Match foo. (* no need to disambiguate *) End A. Module B. - Inductive foo := f. + #[universes(template)] 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/StringSyntax.out b/test-suite/output/StringSyntax.out index bbc936766d..c7e6ef950e 100644 --- a/test-suite/output/StringSyntax.out +++ b/test-suite/output/StringSyntax.out @@ -1,4 +1,4 @@ -Monomorphic byte_rect = +byte_rect = fun (P : byte -> Type) (f : P "000") (f0 : P "001") (f1 : P "002") (f2 : P "003") (f3 : P "004") (f4 : P "005") (f5 : P "006") (f6 : P "007") (f7 : P "008") (f8 : P "009") (f9 : P "010") (f10 : P "011") (f11 : P "012") (f12 : P "013") (f13 : P "014") (f14 : P "015") (f15 : P "016") (f16 : P "017") (f17 : P "018") (f18 : P "019") (f19 : P "020") (f20 : P "021") (f21 : P "022") (f22 : P "023") (f23 : P "024") (f24 : P "025") (f25 : P "026") (f26 : P "027") (f27 : P "028") (f28 : P "029") (f29 : P "030") (f30 : P "031") (f31 : P " ") (f32 : P "!") (f33 : P """") (f34 : P "#") (f35 : P "$") (f36 : P "%") (f37 : P "&") (f38 : P "'") (f39 : P "(") (f40 : P ")") (f41 : P "*") (f42 : P "+") (f43 : P ",") (f44 : P "-") (f45 : P ".") (f46 : P "/") (f47 : P "0") (f48 : P "1") (f49 : P "2") (f50 : P "3") (f51 : P "4") (f52 : P "5") (f53 : P "6") (f54 : P "7") (f55 : P "8") (f56 : P "9") (f57 : P ":") (f58 : P ";") (f59 : P "<") (f60 : P "=") (f61 : P ">") (f62 : P "?") (f63 : P "@") (f64 : P "A") (f65 : P "B") (f66 : P "C") (f67 : P "D") (f68 : P "E") (f69 : P "F") (f70 : P "G") (f71 : P "H") (f72 : P "I") (f73 : P "J") (f74 : P "K") (f75 : P "L") (f76 : P "M") (f77 : P "N") (f78 : P "O") (f79 : P "P") (f80 : P "Q") (f81 : P "R") (f82 : P "S") (f83 : P "T") (f84 : P "U") (f85 : P "V") (f86 : P "W") (f87 : P "X") (f88 : P "Y") (f89 : P "Z") (f90 : P "[") (f91 : P "\") (f92 : P "]") (f93 : P "^") (f94 : P "_") (f95 : P "`") (f96 : P "a") (f97 : P "b") (f98 : P "c") (f99 : P "d") (f100 : P "e") (f101 : P "f") (f102 : P "g") (f103 : P "h") (f104 : P "i") (f105 : P "j") (f106 : P "k") (f107 : P "l") (f108 : P "m") (f109 : P "n") (f110 : P "o") (f111 : P "p") (f112 : P "q") (f113 : P "r") (f114 : P "s") (f115 : P "t") (f116 : P "u") (f117 : P "v") (f118 : P "w") (f119 : P "x") (f120 : P "y") (f121 : P "z") (f122 : P "{") (f123 : P "|") (f124 : P "}") (f125 : P "~") (f126 : P "127") (f127 : P "128") (f128 : P "129") (f129 : P "130") (f130 : P "131") (f131 : P "132") (f132 : P "133") (f133 : P "134") (f134 : P "135") (f135 : P "136") (f136 : P "137") (f137 : P "138") (f138 : P "139") (f139 : P "140") (f140 : P "141") (f141 : P "142") (f142 : P "143") (f143 : P "144") (f144 : P "145") (f145 : P "146") (f146 : P "147") (f147 : P "148") (f148 : P "149") (f149 : P "150") (f150 : P "151") (f151 : P "152") (f152 : P "153") (f153 : P "154") (f154 : P "155") (f155 : P "156") (f156 : P "157") (f157 : P "158") (f158 : P "159") (f159 : P "160") (f160 : P "161") (f161 : P "162") (f162 : P "163") (f163 : P "164") (f164 : P "165") (f165 : P "166") (f166 : P "167") (f167 : P "168") (f168 : P "169") (f169 : P "170") (f170 : P "171") (f171 : P "172") (f172 : P "173") (f173 : P "174") (f174 : P "175") (f175 : P "176") (f176 : P "177") (f177 : P "178") (f178 : P "179") (f179 : P "180") (f180 : P "181") (f181 : P "182") (f182 : P "183") (f183 : P "184") (f184 : P "185") (f185 : P "186") (f186 : P "187") @@ -435,7 +435,7 @@ end byte_rect is not universe polymorphic Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope] -Monomorphic byte_rec = +byte_rec = fun P : byte -> Set => byte_rect P : forall P : byte -> Set, P "000" -> @@ -610,7 +610,7 @@ fun P : byte -> Set => byte_rect P byte_rec is not universe polymorphic Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope] -Monomorphic byte_ind = +byte_ind = fun (P : byte -> Prop) (f : P "000") (f0 : P "001") (f1 : P "002") (f2 : P "003") (f3 : P "004") (f4 : P "005") (f5 : P "006") (f6 : P "007") (f7 : P "008") (f8 : P "009") (f9 : P "010") (f10 : P "011") (f11 : P "012") (f12 : P "013") (f13 : P "014") (f14 : P "015") (f15 : P "016") (f16 : P "017") (f17 : P "018") (f18 : P "019") (f19 : P "020") (f20 : P "021") (f21 : P "022") (f22 : P "023") (f23 : P "024") (f24 : P "025") (f25 : P "026") (f26 : P "027") (f27 : P "028") (f28 : P "029") (f29 : P "030") (f30 : P "031") (f31 : P " ") (f32 : P "!") (f33 : P """") (f34 : P "#") (f35 : P "$") (f36 : P "%") (f37 : P "&") (f38 : P "'") (f39 : P "(") (f40 : P ")") (f41 : P "*") (f42 : P "+") (f43 : P ",") (f44 : P "-") (f45 : P ".") (f46 : P "/") (f47 : P "0") (f48 : P "1") (f49 : P "2") (f50 : P "3") (f51 : P "4") (f52 : P "5") (f53 : P "6") (f54 : P "7") (f55 : P "8") (f56 : P "9") (f57 : P ":") (f58 : P ";") (f59 : P "<") (f60 : P "=") (f61 : P ">") (f62 : P "?") (f63 : P "@") (f64 : P "A") (f65 : P "B") (f66 : P "C") (f67 : P "D") (f68 : P "E") (f69 : P "F") (f70 : P "G") (f71 : P "H") (f72 : P "I") (f73 : P "J") (f74 : P "K") (f75 : P "L") (f76 : P "M") (f77 : P "N") (f78 : P "O") (f79 : P "P") (f80 : P "Q") (f81 : P "R") (f82 : P "S") (f83 : P "T") (f84 : P "U") (f85 : P "V") (f86 : P "W") (f87 : P "X") (f88 : P "Y") (f89 : P "Z") (f90 : P "[") (f91 : P "\") (f92 : P "]") (f93 : P "^") (f94 : P "_") (f95 : P "`") (f96 : P "a") (f97 : P "b") (f98 : P "c") (f99 : P "d") (f100 : P "e") (f101 : P "f") (f102 : P "g") (f103 : P "h") (f104 : P "i") (f105 : P "j") (f106 : P "k") (f107 : P "l") (f108 : P "m") (f109 : P "n") (f110 : P "o") (f111 : P "p") (f112 : P "q") (f113 : P "r") (f114 : P "s") (f115 : P "t") (f116 : P "u") (f117 : P "v") (f118 : P "w") (f119 : P "x") (f120 : P "y") (f121 : P "z") (f122 : P "{") (f123 : P "|") (f124 : P "}") (f125 : P "~") (f126 : P "127") (f127 : P "128") (f128 : P "129") (f129 : P "130") (f130 : P "131") (f131 : P "132") (f132 : P "133") (f133 : P "134") (f134 : P "135") (f135 : P "136") (f136 : P "137") (f137 : P "138") (f138 : P "139") (f139 : P "140") (f140 : P "141") (f141 : P "142") (f142 : P "143") (f143 : P "144") (f144 : P "145") (f145 : P "146") (f146 : P "147") (f147 : P "148") (f148 : P "149") (f149 : P "150") (f150 : P "151") (f151 : P "152") (f152 : P "153") (f153 : P "154") (f154 : P "155") (f155 : P "156") (f156 : P "157") (f157 : P "158") (f158 : P "159") (f159 : P "160") (f160 : P "161") (f161 : P "162") (f162 : P "163") (f163 : P "164") (f164 : P "165") (f165 : P "166") (f166 : P "167") (f167 : P "168") (f168 : P "169") (f169 : P "170") (f170 : P "171") (f171 : P "172") (f172 : P "173") (f173 : P "174") (f174 : P "175") (f175 : P "176") (f176 : P "177") (f177 : P "178") (f178 : P "179") (f179 : P "180") (f180 : P "181") (f181 : P "182") (f182 : P "183") (f183 : P "184") (f184 : P "185") (f185 : P "186") (f186 : P "187") diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out index f080f6d0f0..67b65d4b81 100644 --- a/test-suite/output/TranspModtype.out +++ b/test-suite/output/TranspModtype.out @@ -1,15 +1,15 @@ -Monomorphic TrM.A = M.A +TrM.A = M.A : Set TrM.A is not universe polymorphic -Monomorphic OpM.A = M.A +OpM.A = M.A : Set OpM.A is not universe polymorphic -Monomorphic TrM.B = M.B +TrM.B = M.B : Set TrM.B is not universe polymorphic -Monomorphic *** [ OpM.B : Set ] +*** [ OpM.B : Set ] OpM.B is not universe polymorphic diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 4d3f7419e6..0bd6ade690 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -1,37 +1,34 @@ -Polymorphic NonCumulative Inductive Empty@{u} : Type@{u} := -Polymorphic NonCumulative Record PWrap (A : Type@{u}) : Type@{u} := pwrap - { punwrap : A } +Inductive Empty@{u} : Type@{u} := +Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A } PWrap has primitive projections with eta conversion. For PWrap: Argument scope is [type_scope] For pwrap: Argument scopes are [type_scope _] -Polymorphic punwrap@{u} = +punwrap@{u} = fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p : forall A : Type@{u}, PWrap@{u} A -> A (* u |= *) punwrap is universe polymorphic Argument scopes are [type_scope _] -Polymorphic NonCumulative Record RWrap (A : Type@{u}) : Type@{u} := rwrap - { runwrap : A } +Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A } For RWrap: Argument scope is [type_scope] For rwrap: Argument scopes are [type_scope _] -Polymorphic runwrap@{u} = +runwrap@{u} = fun (A : Type@{u}) (r : RWrap@{u} A) => let (runwrap) := r in runwrap : forall A : Type@{u}, RWrap@{u} A -> A (* u |= *) runwrap is universe polymorphic Argument scopes are [type_scope _] -Polymorphic Wrap@{u} = -fun A : Type@{u} => A +Wrap@{u} = fun A : Type@{u} => A : Type@{u} -> Type@{u} (* u |= *) Wrap is universe polymorphic Argument scope is [type_scope] -Polymorphic wrap@{u} = +wrap@{u} = fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap : forall A : Type@{u}, Wrap@{u} A -> A (* u |= *) @@ -39,12 +36,12 @@ fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap wrap is universe polymorphic Arguments A, Wrap are implicit and maximally inserted Argument scopes are [type_scope _] -Polymorphic bar@{u} = nat +bar@{u} = nat : Wrap@{u} Set (* u |= Set < u *) bar is universe polymorphic -Polymorphic foo@{u UnivBinders.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 |= *) @@ -56,7 +53,7 @@ Type@{i} -> Type@{j} = Type@{i} -> Type@{j} : Type@{max(i+1,j+1)} (* {j i} |= *) -Monomorphic mono = Type@{mono.u} +mono = Type@{mono.u} : Type@{mono.u+1} (* {mono.u} |= *) @@ -77,7 +74,7 @@ mono : Type@{mono.u+1} The command has indeed failed with message: Universe u already exists. -Monomorphic bobmorane = +bobmorane = let tt := Type@{UnivBinders.32} in let ff := Type@{UnivBinders.34} in tt -> ff : Type@{max(UnivBinders.31,UnivBinders.33)} @@ -85,21 +82,20 @@ let ff := Type@{UnivBinders.34} in tt -> ff bobmorane is not universe polymorphic The command has indeed failed with message: Universe u already bound. -Polymorphic foo@{E M N} = +foo@{E M N} = Type@{M} -> Type@{N} -> Type@{E} : Type@{max(E+1,M+1,N+1)} (* E M N |= *) foo is universe polymorphic -Polymorphic foo@{u UnivBinders.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 -Polymorphic NonCumulative Inductive Empty@{E} : Type@{E} := -Polymorphic NonCumulative Record PWrap (A : Type@{E}) : Type@{E} := pwrap - { punwrap : A } +Inductive Empty@{E} : Type@{E} := +Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A } PWrap has primitive projections with eta conversion. For PWrap: Argument scope is [type_scope] @@ -119,58 +115,55 @@ The command has indeed failed with message: This object does not support universe names. The command has indeed failed with message: Cannot enforce v < u because u < gU < gV < v -Monomorphic bind_univs.mono = +bind_univs.mono = Type@{bind_univs.mono.u} : Type@{bind_univs.mono.u+1} (* {bind_univs.mono.u} |= *) bind_univs.mono is not universe polymorphic -Polymorphic bind_univs.poly@{u} = Type@{u} +bind_univs.poly@{u} = Type@{u} : Type@{u+1} (* u |= *) bind_univs.poly is universe polymorphic -Polymorphic insec@{v} = -Type@{u} -> Type@{v} +insec@{v} = Type@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* v |= *) insec is universe polymorphic -Polymorphic NonCumulative Inductive insecind@{k} : Type@{k+1} := - inseccstr : Type@{k} -> insecind@{k} +Inductive insecind@{k} : Type@{k+1} := inseccstr : Type@{k} -> insecind@{k} For inseccstr: Argument scope is [type_scope] -Polymorphic insec@{u v} = -Type@{u} -> Type@{v} +insec@{u v} = Type@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* u v |= *) insec is universe polymorphic -Polymorphic NonCumulative Inductive insecind@{u k} : Type@{k+1} := +Inductive insecind@{u k} : Type@{k+1} := inseccstr : Type@{k} -> insecind@{u k} For inseccstr: Argument scope is [type_scope] -Polymorphic insec2@{u} = Prop +insec2@{u} = Prop : Type@{Set+1} (* u |= *) insec2 is universe polymorphic -Polymorphic inmod@{u} = Type@{u} +inmod@{u} = Type@{u} : Type@{u+1} (* u |= *) inmod is universe polymorphic -Polymorphic SomeMod.inmod@{u} = Type@{u} +SomeMod.inmod@{u} = Type@{u} : Type@{u+1} (* u |= *) SomeMod.inmod is universe polymorphic -Polymorphic inmod@{u} = Type@{u} +inmod@{u} = Type@{u} : Type@{u+1} (* u |= *) inmod is universe polymorphic -Polymorphic Applied.infunct@{u v} = +Applied.infunct@{u v} = inmod@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* u v |= *) diff --git a/test-suite/output/Warnings.v b/test-suite/output/Warnings.v index 7465442cab..0eb5db1733 100644 --- a/test-suite/output/Warnings.v +++ b/test-suite/output/Warnings.v @@ -1,5 +1,5 @@ (* Term in warning was not printed in the right environment at some time *) -Record A := { B:Type; b:B->B }. +#[universes(template)] Record A := { B:Type; b:B->B }. Definition a B := {| B:=B; b:=fun x => x |}. Canonical Structure a. diff --git a/test-suite/output/goal_output.out b/test-suite/output/goal_output.out index 3dad2360c4..20568f742a 100644 --- a/test-suite/output/goal_output.out +++ b/test-suite/output/goal_output.out @@ -1,8 +1,8 @@ -Monomorphic Nat.t = nat +Nat.t = nat : Set Nat.t is not universe polymorphic -Monomorphic Nat.t = nat +Nat.t = nat : Set Nat.t is not universe polymorphic diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out index a1326596bb..f545ca679c 100644 --- a/test-suite/output/inference.out +++ b/test-suite/output/inference.out @@ -1,4 +1,4 @@ -Monomorphic P = +P = fun e : option L => match e with | Some cl => Some cl | None => None diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v index 57a4739e9f..209fedc343 100644 --- a/test-suite/output/inference.v +++ b/test-suite/output/inference.v @@ -21,6 +21,6 @@ Print P. (* Note: exact numbers of evars are not important... *) -Inductive T (n:nat) : Type := A : T n. +#[universes(template)] Inductive T (n:nat) : Type := A : T n. Check fun n (y:=A n:T n) => _ _ : T n. Check fun n => _ _ : T n. diff --git a/test-suite/report.sh b/test-suite/report.sh index c5e698232f..cef615266b 100755 --- a/test-suite/report.sh +++ b/test-suite/report.sh @@ -15,7 +15,7 @@ mkdir "$SAVEDIR" FAILMARK="==========> FAILURE <==========" FAILED=$(mktemp /tmp/coq-check-XXXXXX) -find . '(' -path ./bugs/opened -prune ')' -o '(' -name '*.log' -exec grep "$FAILMARK" -q '{}' ';' -print0 ')' > "$FAILED" +find . '(' -name '*.log' -exec grep "$FAILMARK" -q '{}' ';' -print0 ')' > "$FAILED" rsync -a --from0 --files-from="$FAILED" . "$SAVEDIR" cp summary.log "$SAVEDIR"/ diff --git a/test-suite/ssr/elim.v b/test-suite/ssr/elim.v index 908249a369..720f4f6607 100644 --- a/test-suite/ssr/elim.v +++ b/test-suite/ssr/elim.v @@ -33,7 +33,7 @@ Qed. (* The same but without names for variables involved in the generated eq *) Lemma testL3 : forall A (s : seq A), s = s. Proof. -move=> A s; elim branch: s; move: (s) => _. +move=> A s; elim branch: s. match goal with _ : _ = [::] |- [::] = [::] => move: branch => // | _ => fail end. move=> _; match goal with _ : _ = _ :: _ |- _ :: _ = _ :: _ => move: branch => // | _ => fail end. Qed. diff --git a/test-suite/ssr/ipat_clear_if_id.v b/test-suite/ssr/ipat_clear_if_id.v index 7a44db2ea0..cc087a62ad 100644 --- a/test-suite/ssr/ipat_clear_if_id.v +++ b/test-suite/ssr/ipat_clear_if_id.v @@ -8,6 +8,7 @@ Variable v2 : nat -> bool. Lemma test (v3 : nat -> bool) (v4 : bool -> bool) (v5 : bool -> bool) : nat -> nat -> nat -> nat -> True. Proof. +Set Debug Ssreflect. move=> {}/v1 b1 {}/v2 b2 {}/v3 b3 {}/v2/v4/v5 b4. Check b1 : bool. Check b2 : bool. @@ -20,4 +21,12 @@ Check v2 : nat -> bool. by []. Qed. +Lemma test2 (v : True <-> False) : True -> False. +Proof. +move=> {}/v. +Fail Check v. +by []. +Qed. + + End Foo. diff --git a/test-suite/ssr/ipat_fast_any.v b/test-suite/ssr/ipat_fast_any.v new file mode 100644 index 0000000000..a50984c7c0 --- /dev/null +++ b/test-suite/ssr/ipat_fast_any.v @@ -0,0 +1,21 @@ +Require Import ssreflect. + +Goal forall y x : nat, x = y -> x = x. +Proof. +move=> + > ->. match goal with |- forall y, y = y => by [] end. +Qed. + +Goal forall y x : nat, le x y -> x = y. +Proof. +move=> > [|]. + by []. +match goal with |- forall a, _ <= a -> _ = S a => admit end. +Admitted. + +Goal forall y x : nat, le x y -> x = y. +Proof. +move=> y x. +case E: x => >. + admit. +match goal with |- S _ <= y -> S _ = y => admit end. +Admitted. diff --git a/test-suite/ssr/ipat_fastid.v b/test-suite/ssr/ipat_fastid.v new file mode 100644 index 0000000000..b0985a0d2f --- /dev/null +++ b/test-suite/ssr/ipat_fastid.v @@ -0,0 +1,48 @@ +Require Import ssreflect. + +Axiom odd : nat -> Prop. + +Lemma simple : + forall x, 3 <= x -> forall y, odd (y+x) -> x = y -> True. +Proof. +move=> >x_ge_3 >xy_odd. +lazymatch goal with +| |- ?x = ?y -> True => done +end. +Qed. + +Lemma simple2 : + forall x, 3 <= x -> forall y, odd (y+x) -> x = y -> True. +Proof. +move=> >; move=>x_ge_3; move=> >; move=>xy_odd. +lazymatch goal with +| |- ?x = ?y -> True => done +end. +Qed. + + +Definition stuff x := 3 <= x -> forall y, odd (y+x) -> x = y -> True. + +Lemma harder : forall x, stuff x. +Proof. +move=> >x_ge_3 >xy_odd. +lazymatch goal with +| |- ?x = ?y -> True => done +end. +Qed. + +Lemma harder2 : forall x, stuff x. +Proof. +move=> >; move=>x_ge_3;move=> >; move=>xy_odd. +lazymatch goal with +| |- ?x = ?y -> True => done +end. +Qed. + +Lemma homotop : forall x : nat, forall e : x = x, e = e -> True. +Proof. +move=> >eq_ee. +lazymatch goal with +| |- True => done +end. +Qed. diff --git a/test-suite/ssr/ipat_seed.v b/test-suite/ssr/ipat_seed.v new file mode 100644 index 0000000000..e418d66917 --- /dev/null +++ b/test-suite/ssr/ipat_seed.v @@ -0,0 +1,60 @@ +Require Import ssreflect. + +Section foo. + +Variable A : Type. + +Record bar (X : Type) := mk_bar { + a : X * A; + b : A; + c := (a,7); + _ : X; + _ : X +}. + +Inductive baz (X : Type) (Y : Type) : nat -> Type := +| K1 x (e : 0=1) (f := 3) of x=x:>X : baz X Y O +| K2 n of n=n & baz X nat 0 : baz X Y (n+1). + +Axiom Q : nat -> Prop. +Axiom Qx : forall x, Q x. +Axiom my_ind : + forall P : nat -> Prop, P O -> (forall n m (w : P n /\ P m), P (n+m)) -> + forall w, P w. + +Lemma test x : bar nat -> baz nat nat x -> forall n : nat, Q n. +Proof. + +(* record *) +move => [^~ _ccc ]. +Check (refl_equal _ : c_ccc = (a_ccc, 7)). + +(* inductive *) +move=> [^ xxx_ ]. +Check (refl_equal _ : xxx_f = 3). + by []. +Check (refl_equal _ : xxx_n = xxx_n). + +(* eliminator *) +elim/my_ind => [^ wow_ ]. + exact: Qx 0. +Check (wow_w : Q wow_n /\ Q wow_m). +exact: Qx (wow_n + wow_m). + +Qed. + +Arguments mk_bar A x y z w : rename. +Arguments K1 A B a b c : rename. + + +Lemma test2 x : bar nat -> baz nat nat x -> forall n : nat, Q n. +Proof. +move=> [^~ _ccc ]. +Check (refl_equal _ : c_ccc = (x_ccc, 7)). +move=> [^ xxx_ ]. +Check (refl_equal _ : xxx_f = 3). + by []. +Check (refl_equal _ : xxx_n = xxx_n). +Abort. + +End foo. diff --git a/test-suite/ssr/ipat_tac.v b/test-suite/ssr/ipat_tac.v new file mode 100644 index 0000000000..cfef2e37be --- /dev/null +++ b/test-suite/ssr/ipat_tac.v @@ -0,0 +1,38 @@ +Require Import ssreflect. + +Ltac fancy := case; last first. + +Notation fancy := (ltac:( fancy )). + +Ltac replicate n := + let what := fresh "_replicate_" in + move=> what; do n! [ have := what ]; clear what. + +Notation replicate n := (ltac:( replicate n )). + +Lemma foo x (w : nat) (J : bool -> nat -> nat) : exists y, x=0+y. +Proof. +move: (w) => /ltac:(idtac) _. +move: w => /(replicate 6) w1 w2 w3 w4 w5 w6. +move: w1 => /J/fancy [w'||];last exact: false. + move: w' => /J/fancy[w''||]; last exact: false. + by exists x. + by exists x. +by exists x. +Qed. + +Ltac unfld what := rewrite /what. + +Notation "% n" := (ltac:( unfld n )) (at level 0) : ssripat_scope. +Notation "% n" := n : nat_scope. + +Open Scope nat_scope. + + +Definition def := 4. + +Lemma test : True -> def = 4. +Proof. +move=> _ /(% def). +match goal with |- 4 = 4 => reflexivity end. +Qed. diff --git a/test-suite/ssr/ipat_tmp.v b/test-suite/ssr/ipat_tmp.v new file mode 100644 index 0000000000..5f5421ac74 --- /dev/null +++ b/test-suite/ssr/ipat_tmp.v @@ -0,0 +1,22 @@ +Require Import ssreflect ssrbool. + + Axiom eqn : nat -> nat -> bool. + Infix "==" := eqn (at level 40). + Axiom eqP : forall x y : nat, reflect (x = y) (x == y). + + Lemma test1 : + forall x y : nat, x = y -> forall z : nat, y == z -> x = z. + Proof. + by move=> x y + z /eqP <-; apply. + Qed. + + Lemma test2 : forall (x y : nat) (e : x = y), e = e -> x = y. + Proof. + move=> + y + _ => x def_x; exact: (def_x : x = y). + Qed. + + Lemma test3 : + forall x y : nat, x = y -> forall z : nat, y == z -> x = z. + Proof. + move=> ++++ /eqP <- => x y e z; exact: e. + Qed. diff --git a/test-suite/ssr/misc_extended.v b/test-suite/ssr/misc_extended.v new file mode 100644 index 0000000000..81c86f1af4 --- /dev/null +++ b/test-suite/ssr/misc_extended.v @@ -0,0 +1,83 @@ +Require Import ssreflect. + +Require Import List. + +Lemma test_elim_pattern_1 : forall A (l:list A), l ++ nil = l. +Proof. +intros A. +elim/list_ind => [^~ 1 ]. + by []. +match goal with |- (a1 :: l1) ++ nil = a1 :: l1 => idtac end. +Abort. + +Lemma test_elim_pattern_2 : forall A (l:list A), l ++ nil = l. +Proof. +intros. elim: l => [^~ 1 ]. + by []. +match goal with |- (a1 :: l1) ++ nil = a1 :: l1 => idtac end. +Abort. + +Lemma test_elim_pattern_3 : forall A (l:list A), l ++ nil = l. +Proof. +intros. elim: l => [ | x l' IH ]. + by []. +match goal with |- (x :: l') ++ nil = x :: l' => idtac end. +Abort. + + +Generalizable Variables A. + +Class Inhab (A:Type) : Type := + { arbitrary : A }. + +Lemma test_intro_typeclass_1 : forall A `{Inhab A} (l1 l2:list A), l2 = nil -> l1 ++ l2 = l1. +Proof. +move =>> H. + match goal with |- _ = _ => idtac end. +Abort. + +Lemma test_intro_typeclass_2 : forall A `{Inhab A} (x:A), x = arbitrary -> x = arbitrary. +Proof. +move =>> H. + match goal with |- _ = _ => idtac end. +Abort. + +Lemma test_intro_temporary_1 : forall A (l1 l2:list A), l2 = nil -> l1 ++ l2 = l1. +Proof. +move => A + l2. + match goal with |- forall l1, l2 = nil -> l1 ++ l2 = l1 => idtac end. +Abort. + +Lemma test_intro_temporary_2 : forall A `{Inhab A} (l1 l2:list A), l2 = nil -> l1 ++ l2 = l1. +Proof. +move => > E. + match goal with |- _ = _ => idtac end. +Abort. + +Lemma test_dispatch : (forall x:nat, x= x )/\ (forall y:nat, y = y). +Proof. +intros. split => [ a | b ]. + match goal with |- a = a => by [] end. +match goal with |- b = b => by [] end. +Abort. + +Lemma test_tactics_as_view_1 : forall A (l1:list A), nil ++ l1 = l1. +Proof. +move => /ltac:(simpl). +Abort. + +Lemma test_tactics_as_view_2 : forall A, (forall (l1:list A), nil ++ l1 = l1) /\ (nil ++ nil = @nil A). +Proof. +move => A. +(* TODO: I want to do [split =>.] as a temporary step in setting up my script, + but this syntax does not seem to be supported. Can't we have an empty ipat? + Note that I can do [split => [ | ]]*) +split => [| /ltac:(simpl)]. +Abort. + +Notation "%%" := (ltac:(simpl)) : ssripat_scope. + +Lemma test_tactics_as_view_3 : forall A, (forall (l1:list A), nil ++ l1 = l1) /\ (nil ++ nil = @nil A). +Proof. +move => /ltac:(split) [ | /%% ]. +Abort. diff --git a/test-suite/ssr/misc_tc.v b/test-suite/ssr/misc_tc.v new file mode 100644 index 0000000000..4db45b743a --- /dev/null +++ b/test-suite/ssr/misc_tc.v @@ -0,0 +1,30 @@ +Require Import ssreflect List. + +Generalizable Variables A B. + +Class Inhab (A:Type) : Type := + { arbitrary : A }. + +Lemma test_intro_typeclass_1 : forall A `{Inhab A} (x:A), x = arbitrary -> x = arbitrary. +Proof. +move =>> H. (* introduces [H:x=arbitrary] because first non dependent hypothesis *) +Abort. + +Lemma test_intro_typeclass_2 : forall A `{Inhab A} (l1 l2:list A), l2 = nil -> l1 ++ l2 = l1. +Proof. +move =>> H. (* introduces [Inhab A] automatically because it is a typeclass instance *) +Abort. + +Lemma test_intro_typeclass_3 : forall `{Inhab A, Inhab B} (x:A) (y:B), True -> x = x. +Proof. (* Above types [A] and [B] are implicitly quantified *) +move =>> y H. (* introduces the two typeclass instances automatically *) +Abort. + +Class Foo `{Inhab A} : Type := + { foo : A }. + +Lemma test_intro_typeclass_4 : forall `{Foo A}, True -> True. +Proof. (* Above, [A] and [{Inhab A}] are implicitly quantified *) +move =>> H. (* introduces [A] and [Inhab A] because they are dependently used, + and introduce [Foo A] automatically because it is an instance. *) +Abort. diff --git a/test-suite/stm/classify_set_proof_mode_9093.v b/test-suite/stm/classify_set_proof_mode_9093.v new file mode 100644 index 0000000000..d3f73ff435 --- /dev/null +++ b/test-suite/stm/classify_set_proof_mode_9093.v @@ -0,0 +1,9 @@ +(* -*- coq-prog-args: ("-async-proofs" "on" "-noinit"); -*- *) + +Declare ML Module "ltac_plugin". + +Set Default Proof Mode "Classic". + +Goal Prop. + idtac. +Abort. diff --git a/test-suite/stm/delayed_restrict_univs_9093.v b/test-suite/stm/delayed_restrict_univs_9093.v new file mode 100644 index 0000000000..6ca36da4b0 --- /dev/null +++ b/test-suite/stm/delayed_restrict_univs_9093.v @@ -0,0 +1,10 @@ +(* -*- coq-prog-args: ("-async-proofs" "on"); -*- *) + +Unset Universe Polymorphism. + +Ltac exact0 := let x := constr:(Type) in exact 0. + +Lemma lemma_restrict_abstract@{} : (nat * nat)%type. +Proof. split;[exact 0|abstract exact0]. Qed. +(* Debug: 10237:proofworker:0:0 STM: sending back a fat state +Error: Universe {polymorphism.1} is unbound. *) diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v index 52fe98ac07..232ac17cbf 100644 --- a/test-suite/success/Cases.v +++ b/test-suite/success/Cases.v @@ -1873,3 +1873,12 @@ Check match niln in listn O return O=O with niln => eq_refl end. (* (was failing up to May 2017) *) Check fun x => match x with (y,z) as t as w => (y+z,t) = (0,w) end. + +(* A test about binding variables of "in" clause of "match" *) +(* (was failing from 8.5 to Dec 2018) *) + +Check match O in nat return nat with O => O | _ => O end. + +(* Checking that aliases are substituted in the correct order *) + +Check match eq_refl (1,0) in _ = (y as z, y' as z) return z = z with eq_refl => eq_refl end : 0=0. diff --git a/test-suite/unit-tests/printing/proof_diffs_test.ml b/test-suite/unit-tests/printing/proof_diffs_test.ml index 7f9e6cc6e0..d0b8d21b69 100644 --- a/test-suite/unit-tests/printing/proof_diffs_test.ml +++ b/test-suite/unit-tests/printing/proof_diffs_test.ml @@ -51,23 +51,28 @@ let t () = assert_equal ~msg:"has `Removed" ~printer:string_of_bool true has_removed let _ = add_test "diff_str add/remove" t -(* example of a limitation, not really a test *) -let t () = - try - let _ = diff_str "a" ">" in - assert_failure "unlexable string gives an exception" - with _ -> () -let _ = add_test "diff_str unlexable" t - -(* problematic examples for tokenize_string: - comments omitted - quoted string loses quote marks (are escapes supported/handled?) - char constant split into 2 +(* lexer tweaks: + comments are lexed as multiple tokens + strings tokens include begin/end quotes and embedded "" + single multibyte characters returned even if they're not keywords + + inputs that give a lexer failure (but no use case needs them yet): + ".12" + unterminated string + invalid UTF-8 sequences *) let t () = - List.iter (fun x -> cprintf "'%s' " x) (tokenize_string "(* comment *) \"string\" 'c' xx"); - cprintf "\n" -let _ = add_test "tokenize_string examples" t + let str = "(* comment.field *) ?id () \"str\"\"ing\" \\ := Ж > ∃ 'c' xx" in + let toks = tokenize_string str in + (*List.iter (fun x -> cprintf "'%s' " x) toks;*) + (*cprintf "\n";*) + let str_no_white = String.concat "" (String.split_on_char ' ' str) in + assert_equal ~printer:(fun x -> x) str_no_white (String.concat "" toks); + List.iter (fun s -> + assert_equal ~msg:("'" ^ s ^ "' is a single token") ~printer:string_of_bool true (List.mem s toks)) + [ "(*"; "()"; ":="] + +let _ = add_test "tokenize_string/diff_mode in lexer" t open Pp |