diff options
Diffstat (limited to 'test-suite')
22 files changed, 277 insertions, 22 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 954a922c8c..dece21885c 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -62,6 +62,10 @@ coqtopbyte := $(BIN)coqtop.byte -q coqc_interactive := $(coqc) -test-mode -async-proofs-cache force coqdep := $(BIN)coqdep +# This is the convention for coq_makefile +OPT=-$(BEST) +export OPT + VERBOSE?= SHOW := $(if $(VERBOSE),@true,@echo) HIDE := $(if $(VERBOSE),,@) diff --git a/test-suite/bugs/closed/HoTT_coq_107.v b/test-suite/bugs/closed/HoTT_coq_107.v index fa4072a8f6..91f5c423a5 100644 --- a/test-suite/bugs/closed/HoTT_coq_107.v +++ b/test-suite/bugs/closed/HoTT_coq_107.v @@ -2,6 +2,7 @@ (* File reduced by coq-bug-finder from 4897 lines to 2605 lines, then from 2297 lines to 236 lines, then from 239 lines to 137 lines, then from 118 lines to 67 lines, then from 520 lines to 76 lines. *) (** Note: The bug here is the same as the #113, that is, HoTT_coq_113.v *) Require Import Coq.Init.Logic. +Require Import Coq.Init.Ltac. Global Set Universe Polymorphism. Global Set Asymmetric Patterns. Set Implicit Arguments. diff --git a/test-suite/bugs/closed/bug_12045.v b/test-suite/bugs/closed/bug_12045.v new file mode 100644 index 0000000000..4e416778a9 --- /dev/null +++ b/test-suite/bugs/closed/bug_12045.v @@ -0,0 +1,19 @@ +(* Check enough reduction happens in the conclusion of an induction scheme *) + +Lemma foo : + forall (P : nat -> Prop), + (forall n, P (S n)) -> + forall n, + (fun e => + IsSucc e -> + P e) n. +Proof. +Admitted. + +Theorem bar : forall n, + IsSucc n -> + True. +Proof. + intros. + Fail induction n using foo. (* was an anomaly *) +Admitted. diff --git a/test-suite/bugs/closed/bug_3881.v b/test-suite/bugs/closed/bug_3881.v index d7e097e326..50e9de60e5 100644 --- a/test-suite/bugs/closed/bug_3881.v +++ b/test-suite/bugs/closed/bug_3881.v @@ -4,6 +4,7 @@ coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (90ed6636dea41486ddf2cc0daead83f9f0788163) *) Generalizable All Variables. Require Import Coq.Init.Notations. +Require Import Coq.Init.Ltac. Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). Notation "A -> B" := (forall (_ : A), B) : type_scope. Axiom admit : forall {T}, T. diff --git a/test-suite/bugs/closed/bug_4527.v b/test-suite/bugs/closed/bug_4527.v index dfb07520f1..cf802eb89b 100644 --- a/test-suite/bugs/closed/bug_4527.v +++ b/test-suite/bugs/closed/bug_4527.v @@ -5,7 +5,7 @@ then from 269 lines to 255 lines *) (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 4.01.0 coqtop version 8.5 (January 2016) *) -Declare ML Module "ltac_plugin". +Require Import Coq.Init.Ltac. Inductive False := . Axiom proof_admitted : False. Tactic Notation "admit" := case proof_admitted. diff --git a/test-suite/bugs/closed/bug_4533.v b/test-suite/bugs/closed/bug_4533.v index d2f9fb9099..2d628f414d 100644 --- a/test-suite/bugs/closed/bug_4533.v +++ b/test-suite/bugs/closed/bug_4533.v @@ -5,7 +5,7 @@ then from 285 lines to 271 lines *) (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 4.01.0 coqtop version 8.5 (January 2016) *) -Declare ML Module "ltac_plugin". +Require Import Coq.Init.Ltac. Inductive False := . Axiom proof_admitted : False. Tactic Notation "admit" := case proof_admitted. diff --git a/test-suite/bugs/closed/bug_4544.v b/test-suite/bugs/closed/bug_4544.v index e9e9c552f6..213c91bfa0 100644 --- a/test-suite/bugs/closed/bug_4544.v +++ b/test-suite/bugs/closed/bug_4544.v @@ -2,7 +2,7 @@ (* File reduced by coq-bug-finder from original input, then from 2553 lines to 1932 lines, then from 1946 lines to 1932 lines, then from 2467 lines to 1002 lines, then from 1016 lines to 1002 lines *) (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 4.01.0 coqtop version 8.5 (January 2016) *) -Declare ML Module "ltac_plugin". +Require Import Coq.Init.Ltac. Inductive False := . Axiom proof_admitted : False. Tactic Notation "admit" := case proof_admitted. diff --git a/test-suite/bugs/closed/bug_5359.v b/test-suite/bugs/closed/bug_5359.v index 1f202e4396..36f2ec5891 100644 --- a/test-suite/bugs/closed/bug_5359.v +++ b/test-suite/bugs/closed/bug_5359.v @@ -90,7 +90,7 @@ Goal False. (Ring_polynom.PEX Z 2))) (Ring_polynom.PEmul (Ring_polynom.PEX Z 3) (Ring_polynom.PEX Z 3)))) :: nil)%list ) in - Nsatz.nsatz_compute + NsatzTactic.nsatz_compute (@cons _ (@Ring_polynom.PEc _ sugar) (@cons _ (@Ring_polynom.PEc _ nparams) (@cons _ (@Ring_polynom.PEpow _ reified_goal power) reified_givens))). let sugar := constr:( 0%Z ) in @@ -214,6 +214,6 @@ Goal False. (Ring_polynom.PEX Z 2))) (Ring_polynom.PEmul (Ring_polynom.PEX Z 3) (Ring_polynom.PEX Z 3)))) :: nil)%list ) in - Nsatz.nsatz_compute + NsatzTactic.nsatz_compute (@cons _ (@Ring_polynom.PEc _ sugar) (@cons _ (@Ring_polynom.PEc _ nparams) (@cons _ (@Ring_polynom.PEpow _ reified_goal power) reified_givens))). Abort. diff --git a/test-suite/bugs/closed/bug_5445.v b/test-suite/bugs/closed/bug_5445.v new file mode 100644 index 0000000000..deaf174661 --- /dev/null +++ b/test-suite/bugs/closed/bug_5445.v @@ -0,0 +1,11 @@ +Require Import Coq.nsatz.NsatzTactic. +(** Ensure that loading the nsatz tactic doesn't load the reals *) +Fail Module M := Coq.Reals.Rdefinitions. +(** Ensure that loading the nsatz tactic doesn't load classic *) +Fail Check Coq.Logic.Classical_Prop.classic. +(** Ensure that this test-case hasn't messed up about the location of the reals / how to check for them *) +Require Coq.Reals.Rdefinitions. +Module M := Coq.Reals.Rdefinitions. +(** Ensure that this test-case hasn't messed up about the location of classic / how to check for it *) +Require Coq.Logic.Classical_Prop. +Check Coq.Logic.Classical_Prop.classic. diff --git a/test-suite/bugs/closed/bug_6661.v b/test-suite/bugs/closed/bug_6661.v index 28a9ffc7bd..0f4ae2b4c5 100644 --- a/test-suite/bugs/closed/bug_6661.v +++ b/test-suite/bugs/closed/bug_6661.v @@ -7,6 +7,7 @@ Require Export Coq.Init.Notations. +Require Export Coq.Init.Ltac. Notation "'∏' x .. y , P" := (forall x, .. (forall y, P) ..) (at level 200, x binder, y binder, right associativity) : type_scope. Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..) diff --git a/test-suite/bugs/closed/bug_7812.v b/test-suite/bugs/closed/bug_7812.v new file mode 100644 index 0000000000..a714eea81d --- /dev/null +++ b/test-suite/bugs/closed/bug_7812.v @@ -0,0 +1,30 @@ +Module Foo. + Definition binary A := A -> A -> Prop. + + Definition inter A (R1 R2 : binary A): binary A := + fun (x y:A) => R1 x y /\ R2 x y. +End Foo. + +Module Simple_sparse_proof. + Parameter node : Type. + Parameter graph : Type. + Parameter has_edge : graph -> node -> node -> Prop. + Implicit Types x y z : node. + Implicit Types G : graph. + + Parameter mem : forall A, A -> list A -> Prop. + Hypothesis mem_nil : forall x, mem node x nil = False. + + Definition notin (l: list node): node -> node -> Prop := + fun x y => ~ mem node x l /\ ~ mem node y l. + + Definition edge_notin G l : node -> node -> Prop := + Foo.inter node (has_edge G) (notin l). + + Hint Unfold Foo.inter notin edge_notin : rel_crush. + + Lemma edge_notin_nil G : forall x y, edge_notin G nil x y <-> has_edge G x y. + Proof. + intros. autounfold with rel_crush. rewrite !mem_nil. tauto. + Qed. +End Simple_sparse_proof. diff --git a/test-suite/complexity/ConstructiveCauchyRealsPerformance.v b/test-suite/complexity/ConstructiveCauchyRealsPerformance.v new file mode 100644 index 0000000000..c901334da9 --- /dev/null +++ b/test-suite/complexity/ConstructiveCauchyRealsPerformance.v @@ -0,0 +1,149 @@ +(* Here we give some functions that compute non-rational reals, + to measure the computation speed. *) +(* Expected time < 5.00s *) + +Require Import QArith Qabs. +Require Import ConstructiveCauchyRealsMult. + +Local Open Scope CReal_scope. + +Definition approx_sqrt_Q (q : Q) (n : positive) : Q + := let (k,j) := q in + match k with + | Z0 => 0 + | Z.pos i => Z.pos (Pos.sqrt (i*j*n*n)) # (j*n) + | Z.neg i => 0 (* unused *) + end. + +(* Approximation of the square root from below, + improves the convergence modulus. *) +Lemma approx_sqrt_Q_le_below : forall (q : Q) (n : positive), + Qle 0 q -> Qle (approx_sqrt_Q q n * approx_sqrt_Q q n) q. +Proof. + intros. destruct q as [k j]. unfold approx_sqrt_Q. + destruct k as [|i|i]. apply Z.le_refl. + pose proof (Pos.sqrt_spec (i * j * n * n)). simpl in H0. + destruct H0 as [H0 _]. + unfold Qle, Qmult, Qnum, Qden. + rewrite <- Pos2Z.inj_mul, <- Pos2Z.inj_mul, <- Pos2Z.inj_mul. + apply Pos2Z.pos_le_pos. rewrite (Pos.mul_comm i (j * n * (j * n))). + rewrite <- (Pos.mul_comm j), <- (Pos.mul_assoc j), <- (Pos.mul_assoc j). + apply Pos.mul_le_mono_l. + apply (Pos.le_trans _ _ _ H0). + rewrite <- (Pos.mul_comm n), <- (Pos.mul_assoc n). + apply Pos.mul_le_mono_l. + rewrite (Pos.mul_comm i j), <- Pos.mul_assoc, <- Pos.mul_assoc. + apply Pos.mul_le_mono_l. rewrite Pos.mul_comm. apply Pos.le_refl. + exfalso. unfold Qle, Z.le in H; simpl in H. exact (H eq_refl). +Qed. + +Require Import Lia. + +Lemma approx_sqrt_Q_le_below_lia : forall (q : Q) (n : positive), + (0 <= q)%Q -> (approx_sqrt_Q q n * approx_sqrt_Q q n <= q)%Q. +Proof. + intros. destruct q as [k j]. unfold approx_sqrt_Q. + destruct k as [|i|i]. + - apply Z.le_refl. + - unfold Qle, Qmult, Qnum, Qden. + pose proof (Pos.sqrt_spec (i * j * n * n)) as Hsqrt; simpl in Hsqrt. + destruct Hsqrt as [Hsqrt _]; apply (Pos.mul_le_mono_l j) in Hsqrt. + lia. + - unfold Qle, Qnum, Qden in H; lia. +Qed. + +Print Assumptions approx_sqrt_Q_le_below_lia. + +Lemma approx_sqrt_Q_lt_above : forall (q : Q) (n : positive), + Qle 0 q -> Qlt q ((approx_sqrt_Q q n + (1#n)) * (approx_sqrt_Q q n + (1#n))). +Proof. + intros. destruct q as [k j]. unfold approx_sqrt_Q. + destruct k as [|i|i]. reflexivity. + 2: exfalso; unfold Qle, Z.le in H; simpl in H; exact (H eq_refl). + pose proof (Pos.sqrt_spec (i * j * n * n)). simpl in H0. + destruct H0 as [_ H0]. + apply (Qlt_le_trans + _ (((Z.pos ((Pos.sqrt (i * j * n * n)) + 1) # j * n)) + * ((Z.pos ((Pos.sqrt (i * j * n * n)) + 1) # j * n)))). + unfold Qlt, Qmult, Qnum, Qden. + rewrite <- Pos2Z.inj_mul, <- Pos2Z.inj_mul, <- Pos2Z.inj_mul. + apply Pos2Z.pos_lt_pos. + rewrite Pos.mul_comm, <- Pos.mul_assoc, <- Pos.mul_assoc, Pos.mul_comm. + apply Pos.mul_lt_mono_r. rewrite Pplus_one_succ_r in H0. + refine (Pos.le_lt_trans _ _ _ _ H0). rewrite Pos.mul_comm. + apply Pos.mul_le_mono_r. + rewrite <- Pos.mul_assoc, (Pos.mul_comm i), <- Pos.mul_assoc. + apply Pos.mul_le_mono_l. rewrite Pos.mul_comm. apply Pos.le_refl. + setoid_replace (1#n)%Q with (Z.pos j#j*n)%Q. 2: reflexivity. + rewrite Qinv_plus_distr. + unfold Qle, Qmult, Qnum, Qden. apply Z.mul_le_mono_nonneg_r. + discriminate. apply Z.mul_le_mono_nonneg. + discriminate. 2: discriminate. + rewrite Pos2Z.inj_add. apply Z.add_le_mono_l. + apply Pos2Z.pos_le_pos. destruct j; discriminate. + rewrite Pos2Z.inj_add. apply Z.add_le_mono_l. + apply Pos2Z.pos_le_pos. destruct j; discriminate. +Qed. + +Lemma approx_sqrt_Q_pos : forall (q : Q) (n : positive), + Qle 0 q -> Qle 0 (approx_sqrt_Q q n). +Proof. + intros. unfold approx_sqrt_Q. destruct q, Qnum. + apply Qle_refl. discriminate. apply Qle_refl. +Qed. + +Lemma Qsqrt_lt : forall q r :Q, + (0 <= r -> q*q < r*r -> q < r)%Q. +Proof. + intros. destruct (Q_dec q r). destruct s. exact q0. + - exfalso. apply (Qlt_not_le _ _ H0). apply (Qle_trans _ (q * r)). + apply Qmult_le_compat_r. apply Qlt_le_weak, q0. exact H. + rewrite Qmult_comm. + apply Qmult_le_compat_r. apply Qlt_le_weak, q0. + apply (Qle_trans _ r _ H). apply Qlt_le_weak, q0. + - exfalso. rewrite q0 in H0. exact (Qlt_irrefl _ H0). +Qed. + +Lemma approx_sqrt_Q_cauchy : + forall q:Q, QCauchySeq (approx_sqrt_Q q) id. +Proof. + intro q. destruct q as [k j]. destruct k. + - intros n a b H H0. reflexivity. + - assert (forall n a b, Pos.le n b -> + (approx_sqrt_Q (Z.pos p # j) a - approx_sqrt_Q (Z.pos p # j) b + < 1 # n)%Q). + { intros. rewrite <- (Qplus_lt_r _ _ (approx_sqrt_Q (Z.pos p # j) b)). + ring_simplify. apply Qsqrt_lt. + apply (Qle_trans _ (0+(1#n))). rewrite Qplus_0_l. discriminate. + apply Qplus_le_l. apply approx_sqrt_Q_pos. discriminate. + apply (Qle_lt_trans _ (Z.pos p # j)). + apply approx_sqrt_Q_le_below. discriminate. + apply (Qlt_le_trans _ ((approx_sqrt_Q (Z.pos p # j) b + (1 # b)) * + (approx_sqrt_Q (Z.pos p # j) b + (1 # b)))). + apply approx_sqrt_Q_lt_above. discriminate. + apply (Qle_trans _ ((approx_sqrt_Q (Z.pos p # j) b + (1 # n)) * + (approx_sqrt_Q (Z.pos p # j) b + (1 # b)))). + apply Qmult_le_r. + apply (Qlt_le_trans _ (0+(1#b))). rewrite Qplus_0_l. reflexivity. + apply Qplus_le_l. apply approx_sqrt_Q_pos. discriminate. + apply Qplus_le_r. unfold Qle; simpl. + apply Pos2Z.pos_le_pos, H. + apply Qmult_le_l. + apply (Qlt_le_trans _ (0+(1#n))). rewrite Qplus_0_l. reflexivity. + apply Qplus_le_l. apply approx_sqrt_Q_pos. discriminate. + apply Qplus_le_r. unfold Qle; simpl. + apply Pos2Z.pos_le_pos, H. } + intros n a b H0 H1. apply Qabs_case. + intros. apply H, H1. + intros. + setoid_replace (- (approx_sqrt_Q (Z.pos p # j) a - approx_sqrt_Q (Z.pos p # j) b))%Q + with (approx_sqrt_Q (Z.pos p # j) b - approx_sqrt_Q (Z.pos p # j) a)%Q. + 2: ring. apply H, H0. + - intros n a b H H0. reflexivity. +Qed. + +Definition CReal_sqrt_Q (q : Q) : CReal + := exist _ (approx_sqrt_Q q) (approx_sqrt_Q_cauchy q). + + +Time Eval vm_compute in (proj1_sig (CReal_sqrt_Q 2) (10 ^ 400)%positive). diff --git a/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired index 4381160a4e..ebe44f3548 100644 --- a/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired +++ b/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired @@ -1,5 +1,5 @@ COQDEP VFILES COQC Slow.v -Slow (real: 0.04, user: 0.02, sys: 0.01, mem: 45512 ko) +Slow.vo (real: 0.04, user: 0.02, sys: 0.01, mem: 45512 ko) COQC Fast.v -Fast (real: 0.41, user: 0.37, sys: 0.04, mem: 395200 ko) +Fast.vo (real: 0.41, user: 0.37, sys: 0.04, mem: 395200 ko) diff --git a/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired index e6af909268..bf17a3e95c 100644 --- a/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired +++ b/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired @@ -1,5 +1,5 @@ COQDEP VFILES COQC Slow.v -Slow (real: 0.40, user: 0.35, sys: 0.04, mem: 394968 ko) +Slow.vo (real: 0.40, user: 0.35, sys: 0.04, mem: 394968 ko) COQC Fast.v -Fast (real: 0.04, user: 0.03, sys: 0.00, mem: 46564 ko) +Fast.vo (real: 0.04, user: 0.03, sys: 0.00, mem: 46564 ko) diff --git a/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired index 72c520218c..c8f35dc1e4 100644 --- a/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired +++ b/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired @@ -2,5 +2,5 @@ After | File Name | Before || Change | % Change -------------------------------------------------------- 0m00.34s | Total | 0m00.49s || -0m00.14s | -30.61% -------------------------------------------------------- -0m00.32s | Fast | 0m00.02s || +0m00.30s | +1500.00% -0m00.02s | Slow | 0m00.47s || -0m00.44s | -95.74%
\ No newline at end of file +0m00.32s | Fast.vo | 0m00.02s || +0m00.30s | +1500.00% +0m00.02s | Slow.vo | 0m00.47s || -0m00.44s | -95.74%
\ No newline at end of file diff --git a/test-suite/output/BadOptionValueType.out b/test-suite/output/BadOptionValueType.out index 34d8518a75..7388982e7f 100644 --- a/test-suite/output/BadOptionValueType.out +++ b/test-suite/output/BadOptionValueType.out @@ -1,8 +1,14 @@ The command has indeed failed with message: Bad type of value for this option: expected int, got string. The command has indeed failed with message: -Bad type of value for this option: expected bool, got string. +This is an option. A value must be provided. The command has indeed failed with message: -Bad type of value for this option: expected bool, got int. +Bad type of value for this option: expected string, got int. The command has indeed failed with message: -Bad type of value for this option: expected bool, got int. +This is an option. A value must be provided. +The command has indeed failed with message: +This is a flag. It does not take a value. +The command has indeed failed with message: +This is a flag. It does not take a value. +The command has indeed failed with message: +This option does not support the "Unset" command. diff --git a/test-suite/output/BadOptionValueType.v b/test-suite/output/BadOptionValueType.v index b61c3757ba..12ca7bae21 100644 --- a/test-suite/output/BadOptionValueType.v +++ b/test-suite/output/BadOptionValueType.v @@ -1,4 +1,7 @@ Fail Set Default Timeout "2". +Fail Set Default Timeout. +Fail Set Bullet Behavior 2. +Fail Set Bullet Behavior. Fail Set Debug Eauto "yes". Fail Set Debug Eauto 1. -Fail Set Implicit Arguments 1. +Fail Unset Warnings. diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index e121b5e86c..f48eaac4c9 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -14,6 +14,10 @@ Entry constr:myconstr is : nat [<< # 0 >>] : option nat +[b + c] + : nat +fun a : nat => [a + a] + : nat -> nat [1 {f 1}] : Expr fun (x : nat) (y z : Expr) => [1 + y z + {f x}] @@ -81,18 +85,18 @@ fun x : nat => [x] : nat -> nat ∀ x : nat, x = x : Prop -File "stdin", line 219, characters 0-160: +File "stdin", line 226, characters 0-160: Warning: Notation "∀ _ .. _ , _" was already defined with a different format in scope type_scope. [notation-incompatible-format,parsing] ∀x : nat,x = x : Prop -File "stdin", line 232, characters 0-60: +File "stdin", line 239, characters 0-60: Warning: Notation "_ %%% _" was already defined with a different format. [notation-incompatible-format,parsing] -File "stdin", line 236, characters 0-64: +File "stdin", line 243, characters 0-64: Warning: Notation "_ %%% _" was already defined with a different format. [notation-incompatible-format,parsing] -File "stdin", line 241, characters 0-62: +File "stdin", line 248, characters 0-62: Warning: Lonely notation "_ %%%% _" was already defined with a different format. [notation-incompatible-format,parsing] 3 %% 4 @@ -101,9 +105,9 @@ format. [notation-incompatible-format,parsing] : nat 3 %% 4 : nat -File "stdin", line 269, characters 0-61: +File "stdin", line 276, characters 0-61: Warning: The format modifier is irrelevant for only parsing rules. [irrelevant-format-only-parsing,parsing] -File "stdin", line 273, characters 0-63: +File "stdin", line 280, characters 0-63: Warning: The only parsing modifier has no effect in Reserved Notation. [irrelevant-reserved-notation-only-parsing,parsing] diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 1cf0d919b1..4d4b37a8b2 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -22,6 +22,13 @@ Notation "<< x >>" := x (in custom myconstr at level 3, x custom anotherconstr a Notation "# x" := (Some x) (in custom anotherconstr at level 8, x constr at level 9). Check [ << # 0 >> ]. +(* Now check with global *) + +Axiom c : nat. +Notation "x" := x (in custom myconstr at level 0, x global). +Check [ b + c ]. +Check fun a => [ a + a ]. + End A. Module B. diff --git a/test-suite/output/undeclared_key.out b/test-suite/output/undeclared_key.out new file mode 100644 index 0000000000..ed768751fc --- /dev/null +++ b/test-suite/output/undeclared_key.out @@ -0,0 +1,13 @@ +The command has indeed failed with message: +There is no flag, option or table with this name: "Search Blacklists". +The command has indeed failed with message: +There is no qualid-valued table with this name: "Search Blacklist". +File "stdin", line 3, characters 0-22: +Warning: There is no flag or option with this name: "Search Blacklists". +[unknown-option,option] +The command has indeed failed with message: +There is no string-valued table with this name: "Search Blacklists". +The command has indeed failed with message: +There is no qualid-valued table with this name: "Search Blacklist". +The command has indeed failed with message: +There is no qualid-valued table with this name: "Search Blacklist". diff --git a/test-suite/output/undeclared_key.v b/test-suite/output/undeclared_key.v new file mode 100644 index 0000000000..4134bc8bfa --- /dev/null +++ b/test-suite/output/undeclared_key.v @@ -0,0 +1,6 @@ +Fail Test Search Blacklists. +Fail Test Search Blacklist for foo. +Set Search Blacklists. +Fail Remove Search Blacklists "bar" foo. +Fail Remove Search Blacklist "bar" foo. +Fail Add Search Blacklist "bar" foo. diff --git a/test-suite/success/Scheme.v b/test-suite/success/Scheme.v index 4b928007cf..273cb48295 100644 --- a/test-suite/success/Scheme.v +++ b/test-suite/success/Scheme.v @@ -18,7 +18,7 @@ Check myeq_rew. Check myeq_rew_dep. Check myeq_rew_fwd_dep. Check myeq_rew_r. -Check internal_myeq_sym_involutive. +Check myeq_sym_involutive. Check myeq_rew_r_dep. Check myeq_rew_fwd_r_dep. |