diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_10026.v | 3 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_3754.v (renamed from test-suite/bugs/opened/bug_3754.v) | 4 | ||||
| -rw-r--r-- | test-suite/dune | 2 | ||||
| -rwxr-xr-x | test-suite/misc/changelog.sh | 18 | ||||
| -rw-r--r-- | test-suite/output/Arguments.out | 24 | ||||
| -rw-r--r-- | test-suite/output/Arguments.v | 9 | ||||
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 4 | ||||
| -rw-r--r-- | test-suite/output/Notations4.out | 10 | ||||
| -rw-r--r-- | test-suite/output/Notations4.v | 1 | ||||
| -rw-r--r-- | test-suite/output/bug_9370.out | 12 | ||||
| -rw-r--r-- | test-suite/output/bug_9370.v | 12 | ||||
| -rw-r--r-- | test-suite/success/Notations2.v | 4 | ||||
| -rw-r--r-- | test-suite/success/attribute_syntax.v | 4 |
13 files changed, 95 insertions, 12 deletions
diff --git a/test-suite/bugs/closed/bug_10026.v b/test-suite/bugs/closed/bug_10026.v new file mode 100644 index 0000000000..0d3142d0f2 --- /dev/null +++ b/test-suite/bugs/closed/bug_10026.v @@ -0,0 +1,3 @@ +Require Import Coq.Lists.List. +Set Debug RAKAM. +Check fun _ => fold_right (fun A B => prod A B) unit _. diff --git a/test-suite/bugs/opened/bug_3754.v b/test-suite/bugs/closed/bug_3754.v index 18820b1a4c..7031cbf132 100644 --- a/test-suite/bugs/opened/bug_3754.v +++ b/test-suite/bugs/closed/bug_3754.v @@ -281,5 +281,7 @@ Defined. (factor2 fact)). rewrite <- ap_p_pp; rewrite_moveL_Mp_p. Set Debug Tactic Unification. - Fail rewrite (concat_Ap ff2). + rewrite (concat_Ap ff2). Abort. + +End Factorization. diff --git a/test-suite/dune b/test-suite/dune index c430400ba5..cd33319fa4 100644 --- a/test-suite/dune +++ b/test-suite/dune @@ -20,6 +20,8 @@ ../dev/header.ml ../dev/tools/update-compat.py ../doc/stdlib/index-list.html.template + ; For the changelog test + ../config/coq_config.py (package coq) ; For fake_ide (package coqide-server) diff --git a/test-suite/misc/changelog.sh b/test-suite/misc/changelog.sh new file mode 100755 index 0000000000..8b4a49e577 --- /dev/null +++ b/test-suite/misc/changelog.sh @@ -0,0 +1,18 @@ +#!/bin/sh + +while read line; do + if [ "$line" = "is_a_released_version = False" ]; then + echo "This is not a released version: nothing to test." + exit 0 + fi +done < ../config/coq_config.py + +for d in ../doc/changelog/*; do + if [ -d "$d" ]; then + if [ "$(ls $d/*.rst | wc -l)" != "1" ]; then + echo "Fatal: unreleased changelog entries remain in ${d#../}/" + echo "Include them in doc/sphinx/changes.rst and remove them from doc/changelog/" + exit 1 + fi + fi +done diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index 7074ad2d41..3c1e27ba9d 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -27,7 +27,7 @@ Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] The reduction tactics unfold Nat.sub when the 1st and - 2nd arguments evaluate to a constructor and when applied to 2 arguments + 2nd arguments evaluate to a constructor and when applied to 2 arguments Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat @@ -35,7 +35,7 @@ Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] The reduction tactics unfold Nat.sub when the 1st and - 2nd arguments evaluate to a constructor + 2nd arguments evaluate to a constructor Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub pf : @@ -54,7 +54,7 @@ fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C fcomp is not universe polymorphic 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 +The reduction tactics unfold fcomp when applied to 6 arguments fcomp is transparent Expands to: Constant Arguments.fcomp volatile : nat -> nat @@ -75,7 +75,7 @@ f : T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic Argument scopes are [_ _ nat_scope _ nat_scope] The reduction tactics unfold f when the 3rd, 4th and - 5th arguments evaluate to a constructor + 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 @@ -84,7 +84,7 @@ f is not universe polymorphic Argument T2 is implicit 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 + 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 @@ -93,7 +93,7 @@ f is not universe polymorphic Arguments T1, T2 are implicit 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 + 7th arguments evaluate to a constructor f is transparent Expands to: Constant Arguments.f = forall v : unit, f 0 0 5 v 3 = 2 @@ -104,7 +104,7 @@ f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic The reduction tactics unfold f when the 5th, 6th and - 7th arguments evaluate to a constructor + 7th arguments evaluate to a constructor f is transparent Expands to: Constant Arguments.f forall w : r, w 3 true = tt @@ -115,3 +115,13 @@ w 3 true = tt : Prop The command has indeed failed with message: Extra arguments: _, _. +volatilematch : nat -> nat + +volatilematch is not universe polymorphic +Argument scope is [nat_scope] +The reduction tactics always unfold volatilematch + but avoid exposing match constructs +volatilematch is transparent +Expands to: Constant Arguments.volatilematch + = fun n : nat => volatilematch n + : nat -> nat diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v index 844f96aaa1..b909f1b64c 100644 --- a/test-suite/output/Arguments.v +++ b/test-suite/output/Arguments.v @@ -55,3 +55,12 @@ Arguments w x%F y%B : extra scopes. Check (w $ $ = tt). Fail Arguments w _%F _%B. +Definition volatilematch (n : nat) := + match n with + | O => O + | S p => p + end. + +Arguments volatilematch / n : simpl nomatch. +About volatilematch. +Eval simpl in fun n => volatilematch n. diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 3f0717666c..65c902202d 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -62,7 +62,7 @@ Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] The reduction tactics unfold myplus when the 2nd and - 3rd arguments evaluate to a constructor + 3rd arguments evaluate to a constructor myplus is transparent Expands to: Constant Arguments_renaming.Test1.myplus @myplus @@ -101,7 +101,7 @@ Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] The reduction tactics unfold myplus when the 2nd and - 3rd arguments evaluate to a constructor + 3rd arguments evaluate to a constructor myplus is transparent Expands to: Constant Arguments_renaming.myplus @myplus diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 9d972a68f7..c1b9a2b1c6 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -1,5 +1,15 @@ [< 0 > + < 1 > * < 2 >] : nat +Entry constr:myconstr is +[ "6" RIGHTA + [ ] +| "5" RIGHTA + [ SELF; "+"; NEXT ] +| "4" RIGHTA + [ SELF; "*"; NEXT ] +| "3" RIGHTA + [ "<"; constr:operconstr LEVEL "10"; ">" ] ] + [< b > + < b > * < 2 >] : nat [<< # 0 >>] diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 81c64418cb..d1063bfd04 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -9,6 +9,7 @@ Notation "x + y" := (Nat.add x y) (in custom myconstr at level 5). 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 >]. +Print Custom Grammar myconstr. Axiom a : nat. Notation b := a. diff --git a/test-suite/output/bug_9370.out b/test-suite/output/bug_9370.out new file mode 100644 index 0000000000..0ff151c8b4 --- /dev/null +++ b/test-suite/output/bug_9370.out @@ -0,0 +1,12 @@ +1 subgoal + + ============================ + 1 = 1 +1 subgoal + + ============================ + 1 = 1 +1 subgoal + + ============================ + 1 = 1 diff --git a/test-suite/output/bug_9370.v b/test-suite/output/bug_9370.v new file mode 100644 index 0000000000..a7f4b7c23e --- /dev/null +++ b/test-suite/output/bug_9370.v @@ -0,0 +1,12 @@ +Require Import Reals. +Open Scope R_scope. +Goal 1/1=1. +Proof. + field_simplify (1/1). +Show. + field_simplify. +Show. + field_simplify. +Show. + reflexivity. +Qed. diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v index 2533a39cc4..d047f7560e 100644 --- a/test-suite/success/Notations2.v +++ b/test-suite/success/Notations2.v @@ -151,8 +151,8 @@ Module M16. Local Notation "##" := 0 (in custom foo2). (* Test Print Grammar *) - Print Grammar foo. - Print Grammar foo2. + Print Custom Grammar foo. + Print Custom Grammar foo2. End M16. (* Example showing the need for strong evaluation of diff --git a/test-suite/success/attribute_syntax.v b/test-suite/success/attribute_syntax.v index f4f59a3c16..4717759dec 100644 --- a/test-suite/success/attribute_syntax.v +++ b/test-suite/success/attribute_syntax.v @@ -20,6 +20,10 @@ Check ι _ ι. Fixpoint f (n: nat) {wf lt n} : nat := _. Reset f. +#[program(true)] +Fixpoint f (n: nat) {wf lt n} : nat := _. +Reset f. + #[deprecated(since="8.9.0")] Ltac foo := foo. |