diff options
Diffstat (limited to 'test-suite')
58 files changed, 1125 insertions, 74 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 32e245e362..b8aac8b6f8 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -192,10 +192,6 @@ PRINT_LOGS?= TRAVIS?= # special because we want to print travis_fold directives ifdef APPVEYOR PRINT_LOGS:=APPVEYOR -else -ifdef CIRCLECI -PRINT_LOGS:=CIRCLECI -endif #CIRCLECI endif #APPVEYOR report: summary.log @@ -519,6 +515,7 @@ $(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG) @echo "TEST $<" $(HIDE){ \ echo $(call log_intro,$<); \ + export BIN="$(BIN)"; \ export coqc="$(coqc)"; \ export coqtop="$(coqtop)"; \ export coqdep="$(coqdep)"; \ diff --git a/test-suite/bugs/closed/2733.v b/test-suite/bugs/closed/2733.v index 832de4f913..24dd30b32e 100644 --- a/test-suite/bugs/closed/2733.v +++ b/test-suite/bugs/closed/2733.v @@ -16,6 +16,21 @@ match k,l with |B,l' => Bcons true (Ncons 0 l') end. +(* At some time, the success of trullynul was dependent on the name of + the variables! *) + +Definition trullynul2 k {a} (l : alt_list k a) := +match k,l with + |N,l' => Ncons 0 (Bcons true l') + |B,l' => Bcons true (Ncons 0 l') +end. + +Definition trullynul3 k {z} (l : alt_list k z) := +match k,l with + |N,l' => Ncons 0 (Bcons true l') + |B,l' => Bcons true (Ncons 0 l') +end. + Fixpoint app (P : forall {k k'}, alt_list k k' -> alt_list k k') {t1 t2} (l : alt_list t1 t2) {struct l}: forall {t3}, alt_list t2 t3 -> alt_list t1 t3 := match l with diff --git a/test-suite/bugs/closed/4202.v b/test-suite/bugs/closed/4202.v new file mode 100644 index 0000000000..522a3604a3 --- /dev/null +++ b/test-suite/bugs/closed/4202.v @@ -0,0 +1,10 @@ +Parameter g : nat -> Prop. +Axiom a : forall n, g (S n). +Lemma foo (H : True) : exists n, g n /\ g n. +eexists. +clear H. +split. +simple apply a. +(* goal is "g (S ?Goal0@ {H:=H})" while H has long ceased to exist *) +simpl. +Abort. diff --git a/test-suite/bugs/closed/5012.v b/test-suite/bugs/closed/5012.v new file mode 100644 index 0000000000..5326c0fbb1 --- /dev/null +++ b/test-suite/bugs/closed/5012.v @@ -0,0 +1,17 @@ +Class Foo := { foo : Set }. + +Axiom admit : forall {T}, T. + +Global Instance Foo0 : Foo + := {| foo := admit |}. + +Global Instance Foo1 : Foo + := { foo := admit }. + +Existing Class Foo. + +Global Instance Foo2 : Foo + := { foo := admit }. (* Error: Unbound method name foo of class Foo. *) + +Set Warnings "+already-existing-class". +Fail Existing Class Foo. diff --git a/test-suite/bugs/closed/5696.v b/test-suite/bugs/closed/5696.v new file mode 100644 index 0000000000..a20ad1b4da --- /dev/null +++ b/test-suite/bugs/closed/5696.v @@ -0,0 +1,5 @@ +(* Slightly improving interpretation of Ltac subterms in notations *) + +Notation "'var2' x .. y = z ; e" := (ltac:(exact z), (fun x => .. (fun y => e) +..)) (at level 200, x binder, y binder, e at level 220). +Check (var2 a = 1; a). diff --git a/test-suite/bugs/closed/5719.v b/test-suite/bugs/closed/5719.v new file mode 100644 index 0000000000..0fad5f54ea --- /dev/null +++ b/test-suite/bugs/closed/5719.v @@ -0,0 +1,9 @@ +Axiom cons_data_one : + forall (Aone : unit -> Set) (i : unit) (a : Aone i), nat. +Axiom P : nat -> Prop. +Axiom children_data_rect3 : forall {Aone : unit -> Set} + (cons_one_case : forall (i : unit) (b : Aone i), + nat -> nat -> P (cons_data_one Aone i b)), + P 0. +Fail Definition decide_children_equality IH := children_data_rect3 + (fun _ '(existT _ _ _) => match IH with tt => _ end). diff --git a/test-suite/bugs/closed/7695.v b/test-suite/bugs/closed/7695.v new file mode 100644 index 0000000000..42bdb076b6 --- /dev/null +++ b/test-suite/bugs/closed/7695.v @@ -0,0 +1,20 @@ +Require Import Hurkens. + +Universes i j k. +Module Type T. + Parameter T1 : Type@{i+1}. + Parameter e : Type@{j} = T1 : Type@{k}. +End T. + +Module M. + Definition T1 := Type@{j}. + Definition e : Type@{j} = T1 : Type@{k} := eq_refl. +End M. + +Module F (A:T). + Definition bad := TypeNeqSmallType.paradox _ A.e. +End F. + +Set Printing Universes. +Fail Module X := F M. +(* Universe inconsistency. Cannot enforce j <= i because i < Coq.Logic.Hurkens.105 = j. *) diff --git a/test-suite/bugs/closed/7712.v b/test-suite/bugs/closed/7712.v new file mode 100644 index 0000000000..a4e9697fad --- /dev/null +++ b/test-suite/bugs/closed/7712.v @@ -0,0 +1,4 @@ +(* This used to raise an anomaly *) + +Fail Reserved Notation "'[tele_arg' x ';' .. ';' z ]" + (format "[tele_arg '[hv' x .. z ']' ]"). diff --git a/test-suite/bugs/closed/7723.v b/test-suite/bugs/closed/7723.v new file mode 100644 index 0000000000..2162901231 --- /dev/null +++ b/test-suite/bugs/closed/7723.v @@ -0,0 +1,58 @@ +Set Universe Polymorphism. + +Module Segfault. + +Inductive decision_tree : Type := . + +Fixpoint first_satisfying_helper {A B} (f : A -> option B) (ls : list A) : option B + := match ls with + | nil => None + | cons x xs + => match f x with + | Some v => Some v + | None => first_satisfying_helper f xs + end + end. + +Axiom admit : forall {T}, T. +Definition dtree4 : option decision_tree := + match first_satisfying_helper (fun pat : nat => Some pat) (cons 0 nil) + with + | Some _ => admit + | None => admit + end +. +Definition dtree'' := Eval vm_compute in dtree4. (* segfault *) + +End Segfault. + +Module OtherExample. + +Definition bar@{i} := Type@{i}. +Definition foo@{i j} (x y z : nat) := + @id Type@{j} bar@{i}. +Eval vm_compute in foo. + +End OtherExample. + +Module LocalClosure. + +Definition bar@{i} := Type@{i}. + +Definition foo@{i j} (x y z : nat) := + @id (nat -> Type@{j}) (fun _ => Type@{i}). +Eval vm_compute in foo. + +End LocalClosure. + +Require Import Hurkens. +Polymorphic Inductive unit := tt. + +Polymorphic Definition foo := + let x := id tt in (x, x, Type). + +Lemma bad : False. + refine (TypeNeqSmallType.paradox (snd foo) _). + vm_compute. + Fail reflexivity. +Abort. diff --git a/test-suite/bugs/closed/7854.v b/test-suite/bugs/closed/7854.v new file mode 100644 index 0000000000..ab1a29b632 --- /dev/null +++ b/test-suite/bugs/closed/7854.v @@ -0,0 +1,10 @@ +Set Primitive Projections. + +CoInductive stream (A : Type) := cons { + hd : A; + tl : stream A; +}. + +CoFixpoint const {A} (x : A) := cons A x (const x). + +Check (@eq_refl _ (const tt) <<: tl unit (const tt) = const tt). diff --git a/test-suite/bugs/closed/7867.v b/test-suite/bugs/closed/7867.v new file mode 100644 index 0000000000..d0c7902756 --- /dev/null +++ b/test-suite/bugs/closed/7867.v @@ -0,0 +1,4 @@ +(* Was a printer anomaly due to an internal lambda with no binders *) + +Class class := { foo : nat }. +Fail Instance : class := { foo := 0 ; bar := 0 }. diff --git a/test-suite/bugs/closed/7903.v b/test-suite/bugs/closed/7903.v new file mode 100644 index 0000000000..55c7ee99a7 --- /dev/null +++ b/test-suite/bugs/closed/7903.v @@ -0,0 +1,4 @@ +(* Slightly improving interpretation of Ltac subterms in notations *) + +Notation bar x f := (let z := ltac:(exact 1) in (fun x : nat => f)). +Check bar x (x + x). diff --git a/test-suite/bugs/closed/8004.v b/test-suite/bugs/closed/8004.v new file mode 100644 index 0000000000..818639997a --- /dev/null +++ b/test-suite/bugs/closed/8004.v @@ -0,0 +1,47 @@ +Require Export Coq.Program.Tactics Coq.Classes.SetoidTactics Coq.Classes.CMorphisms . + +Set Universe Polymorphism. + +Delimit Scope category_theory_scope with category_theory. +Open Scope category_theory_scope. + +Infix "∧" := prod (at level 80, right associativity) : category_theory_scope. + +Class Setoid A := { + equiv : crelation A; + setoid_equiv :> Equivalence equiv +}. + +Notation "f ≈ g" := (equiv f g) (at level 79) : category_theory_scope. + +Open Scope list_scope. + +Generalizable All Variables. + +Fixpoint list_equiv `{Setoid A} (xs ys : list A) : Type := + match xs, ys with + | nil, nil => True + | x :: xs, y :: ys => x ≈ y ∧ list_equiv xs ys + | _, _ => False + end. + +Axiom proof_admitted : False. +Tactic Notation "admit" := abstract case proof_admitted. + +Program Instance list_equivalence `{Setoid A} : Equivalence list_equiv. +Next Obligation. + repeat intro. + induction x; simpl; split; auto. + reflexivity. +Qed. +Next Obligation. + repeat intro. + generalize dependent y. + induction x, y; simpl; intros; auto. + destruct X; split. + now symmetry. + intuition. +Qed. +Next Obligation. +admit. +Defined. diff --git a/test-suite/bugs/closed/8081.v b/test-suite/bugs/closed/8081.v new file mode 100644 index 0000000000..0f2501aaa8 --- /dev/null +++ b/test-suite/bugs/closed/8081.v @@ -0,0 +1,4 @@ +Section foo. +End foo. +Section foo. +End foo. diff --git a/test-suite/bugs/closed/8106.v b/test-suite/bugs/closed/8106.v new file mode 100644 index 0000000000..a711c5adef --- /dev/null +++ b/test-suite/bugs/closed/8106.v @@ -0,0 +1,4 @@ +(* Was raising an anomaly "already assigned a level" on the second line *) + +Notation "c1 ; c2" := (c1 + c2) (only printing, at level 76, right associativity, c1 at level 76, c2 at level 76). +Notation "c1 ; c2" := (c1 + c2) (only parsing, at level 76, right associativity, c2 at level 76). diff --git a/test-suite/bugs/closed/8119.v b/test-suite/bugs/closed/8119.v new file mode 100644 index 0000000000..c6329a7328 --- /dev/null +++ b/test-suite/bugs/closed/8119.v @@ -0,0 +1,46 @@ +Require Import Coq.Strings.String. + +Section T. + Eval vm_compute in let x := tt in _. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) + Eval vm_compute in let _ := Set in _. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) + Eval vm_compute in let _ := Prop in _. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) +End T. + +Section U0. + Let n : unit := tt. + Eval vm_compute in _. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) + Goal exists tt : unit, tt = tt. eexists. vm_compute. Abort. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) +End U0. + +Section S0. + Let LF : string := String (Coq.Strings.Ascii.Ascii false true false true false false false false) "". + Eval vm_compute in _. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) + Goal exists tt : unit, tt = tt. eexists. vm_compute. Abort. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) +End S0. + +Class T := { }. +Section S1. + Context {p : T}. + Let LF : string := String (Coq.Strings.Ascii.Ascii false true false true false false false false) "". + Eval vm_compute in _. +(* Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/. *) + Goal exists tt : unit, tt = tt. eexists. vm_compute. Abort. +(* Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/. *) +End S1. + +Class M := { m : Type }. +Section S2. + Context {p : M}. + Let LF : string := String (Coq.Strings.Ascii.Ascii false true false true false false false false) "". + Eval vm_compute in _. +(* Error: Anomaly "File "pretyping/vnorm.ml", line 60, characters 9-15: Assertion failed." *) + Goal exists tt : unit, tt = tt. eexists. vm_compute. Abort. +(* Error: Anomaly "File "pretyping/vnorm.ml", line 60, characters 9-15: Assertion failed." *) +End S2. diff --git a/test-suite/bugs/closed/8126.v b/test-suite/bugs/closed/8126.v new file mode 100644 index 0000000000..f52dfc6b47 --- /dev/null +++ b/test-suite/bugs/closed/8126.v @@ -0,0 +1,13 @@ +(* See also output test Notations4.v *) + +Inductive foo := tt. +Bind Scope foo_scope with foo. +Delimit Scope foo_scope with foo. +Notation "'HI'" := tt : foo_scope. +Definition myfoo (x : nat) (y : nat) (z : foo) := y. +Notation myfoo0 := (@myfoo 0). +Notation myfoo01 := (@myfoo0 1). +Check myfoo 0 1 HI. (* prints [myfoo0 1 HI], but should print [myfoo01 HI] *) +Check myfoo0 1 HI. (* prints [myfoo0 1 HI], but should print [myfoo01 HI] *) +Check myfoo01 tt. (* prints [myfoo0 1 HI], but should print [myfoo01 HI] *) +Check myfoo01 HI. (* was failing *) 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 56815d241e..72c520218c 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 @@ -1,6 +1,6 @@ After | File Name | Before || Change | % Change -------------------------------------------------------- -0m00.38s | Total | 0m00.39s || -0m00.01s | -2.56% +0m00.34s | Total | 0m00.49s || -0m00.14s | -30.61% -------------------------------------------------------- -0m00.35s | Slow | 0m00.02s || +0m00.32s | +1649.99% -0m00.03s | Fast | 0m00.37s || -0m00.34s | -91.89%
\ No newline at end of file +0m00.32s | Fast | 0m00.02s || +0m00.30s | +1500.00% +0m00.02s | Slow | 0m00.47s || -0m00.44s | -95.74%
\ No newline at end of file diff --git a/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired b/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired index 18f0f34b28..74dad73332 100644 --- a/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired +++ b/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired @@ -1,9 +1,9 @@ -After | Code | Before || Change | % Change ---------------------------------------------------------------------------------------------------- -0m00.50s | Total | 0m04.17s || -0m03.66s | -87.96% ---------------------------------------------------------------------------------------------------- -0m00.145s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.192s || -0m00.04s | -24.47% -0m00.126s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.] | 0m00.143s || -0m00.01s | -11.88% - N/A | Chars 027 - 068 [Declare~Reduction~comp~:=~nati...] | 0m00.s || +0m00.00s | N/A -0m00.s | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] | N/A || +0m00.00s | N/A -0m00.231s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m03.836s || -0m03.60s | -93.97%
\ No newline at end of file +After | Code | Before || Change | % Change +---------------------------------------------------------------------------------------------------- +0m04.35s | Total | 0m00.58s || +0m03.77s | +649.05% +---------------------------------------------------------------------------------------------------- +0m03.87s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m00.246s || +0m03.62s | +1473.17% +0m00.322s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.189s || +0m00.13s | +70.37% +0m00.16s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.] | 0m00.146s || +0m00.01s | +9.58% +0m00.s | Chars 027 - 068 [Declare~Reduction~comp~:=~nati...] | N/A || +0m00.00s | N/A + N/A | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] | 0m00.s || +0m00.00s | N/A
\ No newline at end of file diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both.log.expected index 975e359b78..159e645512 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both.log.expected @@ -1,6 +1,6 @@ After | File Name | Before || Change | % Change ---------------------------------------------------------------------------------------------- -19m16.05s | Total | 21m25.28s || -2m09.23s | -10.05% +19m16.04s | Total | 21m25.27s || -2m09.23s | -10.05% ---------------------------------------------------------------------------------------------- 4m01.34s | Specific/X25519/C64/ladderstep | 4m59.49s || -0m58.15s | -19.41% 2m48.52s | Specific/solinas32_2e255m765_13limbs/femul | 3m12.95s || -0m24.42s | -12.66% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty.log.expected index fdd5ec21d6..b9739ddb1d 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty.log.expected @@ -1,6 +1,6 @@ Time | File Name ---------------------------------------------------------- -19m16.05s | Total +19m16.04s | Total ---------------------------------------------------------- 4m01.34s | Specific/X25519/C64/ladderstep 3m09.62s | Specific/NISTP256/AMD64/femul diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh index 6737197ee4..78a3f7c63a 100755 --- a/test-suite/coq-makefile/timing/run.sh +++ b/test-suite/coq-makefile/timing/run.sh @@ -5,6 +5,10 @@ set -e . ../template/path-init.sh +# reset MAKEFLAGS so that, e.g., `make -C test-suite -B coq-makefile` doesn't give us issues + +MAKEFLAGS= + cd precomputed-time-tests ./run.sh || exit $? diff --git a/test-suite/coqchk/include_primproj.v b/test-suite/coqchk/include_primproj.v new file mode 100644 index 0000000000..804ba1d378 --- /dev/null +++ b/test-suite/coqchk/include_primproj.v @@ -0,0 +1,13 @@ +(* #7329 *) +Set Primitive Projections. + +Module M. + Module Bar. + Record Box := box { unbox : Type }. + + Axiom foo : Box. + Axiom baz : forall _ : unbox foo, unbox foo. + End Bar. +End M. + +Include M. diff --git a/test-suite/coqdoc/links.html.out b/test-suite/coqdoc/links.html.out index 5e4b676c2f..d2d4d5d764 100644 --- a/test-suite/coqdoc/links.html.out +++ b/test-suite/coqdoc/links.html.out @@ -60,32 +60,32 @@ Various checks for coqdoc <span class="id" title="keyword">Definition</span> <a name="f"><span class="id" title="definition">f</span></a> := <span class="id" title="keyword">∀</span> <span class="id" title="var">C</span>:<span class="id" title="keyword">Prop</span>, <a class="idref" href="Coqdoc.links.html#C"><span class="id" title="variable">C</span></a>.<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="1a1c7f13320341c3638e9edcc3e6389d"><span class="id" title="notation">"</span></a>n ++ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>).<br/> +<span class="id" title="keyword">Notation</span> <a name="f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">"</span></a>n ++ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>).<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="1a1c7f13320341c3638e9edcc3e6389d"><span class="id" title="notation">"</span></a>n ++ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#mult"><span class="id" title="abbreviation">mult</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>). +<span class="id" title="keyword">Notation</span> <a name="f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">"</span></a>n ++ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#mult"><span class="id" title="abbreviation">mult</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>). <br/> -<span class="id" title="keyword">Notation</span> <a name="6b97e27793a3d22f5c0d1dd63170fd68"><span class="id" title="notation">"</span></a>n ** m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 60).<br/> +<span class="id" title="keyword">Notation</span> <a name="f07b3676d96b68749d342542fd80e2b0"><span class="id" title="notation">"</span></a>n ** m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 60).<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="3e01fbae4590c7b7699ff99ce61580e1"><span class="id" title="notation">"</span></a>n ▵ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 60).<br/> +<span class="id" title="keyword">Notation</span> <a name="a647c51c9816a1b44fcfa5312db8344a"><span class="id" title="notation">"</span></a>n ▵ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 60).<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">"</span></a>n '_' ++ 'x' m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 3).<br/> +<span class="id" title="keyword">Notation</span> <a name="3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">"</span></a>n '_' ++ 'x' m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 3).<br/> <br/> -<span class="id" title="keyword">Inductive</span> <a name="eq"><span class="id" title="inductive">eq</span></a> (<span class="id" title="var">A</span>:<span class="id" title="keyword">Type</span>) (<span class="id" title="var">x</span>:<a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a>) : <span class="id" title="var">A</span> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> := <a name="eq_refl"><span class="id" title="constructor">eq_refl</span></a> : <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:></span></a><a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a><br/> +<span class="id" title="keyword">Inductive</span> <a name="eq"><span class="id" title="inductive">eq</span></a> (<span class="id" title="var">A</span>:<span class="id" title="keyword">Type</span>) (<span class="id" title="var">x</span>:<a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a>) : <span class="id" title="var">A</span> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> := <a name="eq_refl"><span class="id" title="constructor">eq_refl</span></a> : <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">=</span></a> <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">:></span></a><a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a><br/> <br/> -<span class="id" title="keyword">where</span> <a name="8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">"</span></a>x = y :> A" := (@<a class="idref" href="Coqdoc.links.html#eq"><span class="id" title="inductive">eq</span></a> <span class="id" title="var">A</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) : <span class="id" title="var">type_scope</span>.<br/> +<span class="id" title="keyword">where</span> <a name="b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">"</span></a>x = y :> A" := (@<a class="idref" href="Coqdoc.links.html#eq"><span class="id" title="inductive">eq</span></a> <span class="id" title="var">A</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) : <span class="id" title="var">type_scope</span>.<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="eq0"><span class="id" title="definition">eq0</span></a> := 0 <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:></span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="eq0"><span class="id" title="definition">eq0</span></a> := 0 <a class="idref" href="Coqdoc.links.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="Coqdoc.links.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">:></span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="548d1059c499c9b2a9b95b07e68c2090"><span class="id" title="notation">"</span></a>( x # y ; .. ; z )" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#pair"><span class="id" title="constructor">pair</span></a> .. (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#pair"><span class="id" title="constructor">pair</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) .. <span class="id" title="var">z</span>).<br/> +<span class="id" title="keyword">Notation</span> <a name="2c0c193cd2aedf7ecdb713db64dbfce6"><span class="id" title="notation">"</span></a>( x # y ; .. ; z )" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#pair"><span class="id" title="constructor">pair</span></a> .. (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#pair"><span class="id" title="constructor">pair</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) .. <span class="id" title="var">z</span>).<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="9f5a1d89cbd4d38f5e289576db7123d1"><span class="id" title="definition">b_α</span></a> := <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="Coqdoc.links.html#548d1059c499c9b2a9b95b07e68c2090"><span class="id" title="notation">(</span></a>0<a class="idref" href="Coqdoc.links.html#548d1059c499c9b2a9b95b07e68c2090"><span class="id" title="notation">#</span></a>0<a class="idref" href="Coqdoc.links.html#548d1059c499c9b2a9b95b07e68c2090"><span class="id" title="notation">;</span></a>0<a class="idref" href="Coqdoc.links.html#548d1059c499c9b2a9b95b07e68c2090"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a>0 <a class="idref" href="Coqdoc.links.html#6b97e27793a3d22f5c0d1dd63170fd68"><span class="id" title="notation">**</span></a> 0<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">))</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="9f5a1d89cbd4d38f5e289576db7123d1"><span class="id" title="definition">b_α</span></a> := <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Coqdoc.links.html#2c0c193cd2aedf7ecdb713db64dbfce6"><span class="id" title="notation">(</span></a>0<a class="idref" href="Coqdoc.links.html#2c0c193cd2aedf7ecdb713db64dbfce6"><span class="id" title="notation">#</span></a>0<a class="idref" href="Coqdoc.links.html#2c0c193cd2aedf7ecdb713db64dbfce6"><span class="id" title="notation">;</span></a>0<a class="idref" href="Coqdoc.links.html#2c0c193cd2aedf7ecdb713db64dbfce6"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a>0 <a class="idref" href="Coqdoc.links.html#f07b3676d96b68749d342542fd80e2b0"><span class="id" title="notation">**</span></a> 0<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">))</span></a>.<br/> <br/> <span class="id" title="keyword">Notation</span> <a name="h"><span class="id" title="abbreviation">h</span></a> := <a class="idref" href="Coqdoc.links.html#a"><span class="id" title="definition">a</span></a>.<br/> @@ -97,7 +97,7 @@ Various checks for coqdoc <span class="id" title="keyword">Variables</span> <a name="test.b'"><span class="id" title="variable">b'</span></a> <a name="test.b2"><span class="id" title="variable">b2</span></a>: <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> <br/> - <span class="id" title="keyword">Notation</span> <a name="4ab0449b36c75cf94e08c5822ea83e3d"><span class="id" title="notation">"</span></a>n + m" := (<span class="id" title="var">n</span> <a class="idref" href="Coqdoc.links.html#3e01fbae4590c7b7699ff99ce61580e1"><span class="id" title="notation">▵</span></a> <span class="id" title="var">m</span>) : <span class="id" title="var">my_scope</span>.<br/> + <span class="id" title="keyword">Notation</span> <a name="2158f15740ce05a939b657be222c26d6"><span class="id" title="notation">"</span></a>n + m" := (<span class="id" title="var">n</span> <a class="idref" href="Coqdoc.links.html#a647c51c9816a1b44fcfa5312db8344a"><span class="id" title="notation">▵</span></a> <span class="id" title="var">m</span>) : <span class="id" title="var">my_scope</span>.<br/> <br/> <span class="id" title="keyword">Delimit</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">my_scope</span> <span class="id" title="keyword">with</span> <span class="id" title="var">my</span>.<br/> @@ -106,19 +106,19 @@ Various checks for coqdoc <span class="id" title="keyword">Notation</span> <a name="l"><span class="id" title="abbreviation">l</span></a> := 0.<br/> <br/> - <span class="id" title="keyword">Definition</span> <a name="ab410a966ac148e9b78c65c6cdf301fd"><span class="id" title="definition">α</span></a> := (0 <a class="idref" href="Coqdoc.links.html#4ab0449b36c75cf94e08c5822ea83e3d"><span class="id" title="notation">+</span></a> <a class="idref" href="Coqdoc.links.html#l"><span class="id" title="abbreviation">l</span></a>)%<span class="id" title="var">my</span>.<br/> + <span class="id" title="keyword">Definition</span> <a name="ab410a966ac148e9b78c65c6cdf301fd"><span class="id" title="definition">α</span></a> := (0 <a class="idref" href="Coqdoc.links.html#2158f15740ce05a939b657be222c26d6"><span class="id" title="notation">+</span></a> <a class="idref" href="Coqdoc.links.html#l"><span class="id" title="abbreviation">l</span></a>)%<span class="id" title="var">my</span>.<br/> <br/> - <span class="id" title="keyword">Definition</span> <a name="a'"><span class="id" title="definition">a'</span></a> <span class="id" title="var">b</span> := <a class="idref" href="Coqdoc.links.html#test.b'"><span class="id" title="variable">b'</span></a><a class="idref" href="Coqdoc.links.html#1a1c7f13320341c3638e9edcc3e6389d"><span class="id" title="notation">++</span></a>0<a class="idref" href="Coqdoc.links.html#1a1c7f13320341c3638e9edcc3e6389d"><span class="id" title="notation">++</span></a><a class="idref" href="Coqdoc.links.html#test.b2"><span class="id" title="variable">b2</span></a> <a class="idref" href="Coqdoc.links.html#347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">_</span></a> <a class="idref" href="Coqdoc.links.html#347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">++</span></a><a class="idref" href="Coqdoc.links.html#347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">x</span></a> <a class="idref" href="Coqdoc.links.html#b"><span class="id" title="variable">b</span></a>.<br/> + <span class="id" title="keyword">Definition</span> <a name="a'"><span class="id" title="definition">a'</span></a> <span class="id" title="var">b</span> := <a class="idref" href="Coqdoc.links.html#test.b'"><span class="id" title="variable">b'</span></a><a class="idref" href="Coqdoc.links.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">++</span></a>0<a class="idref" href="Coqdoc.links.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">++</span></a><a class="idref" href="Coqdoc.links.html#test.b2"><span class="id" title="variable">b2</span></a> <a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">_</span></a> <a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">++</span></a><a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">x</span></a> <a class="idref" href="Coqdoc.links.html#b"><span class="id" title="variable">b</span></a>.<br/> <br/> - <span class="id" title="keyword">Definition</span> <a name="c"><span class="id" title="definition">c</span></a> := <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Specif.html#5bf2050e90b21ebc82dc5463d1ba338e"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Specif.html#5bf2050e90b21ebc82dc5463d1ba338e"><span class="id" title="notation">}+{</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Specif.html#5bf2050e90b21ebc82dc5463d1ba338e"><span class="id" title="notation">}</span></a>.<br/> + <span class="id" title="keyword">Definition</span> <a name="c"><span class="id" title="definition">c</span></a> := <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Specif.html#87727981cdc1579fef00b9d9c1d3b9da"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Specif.html#87727981cdc1579fef00b9d9c1d3b9da"><span class="id" title="notation">}+{</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Specif.html#87727981cdc1579fef00b9d9c1d3b9da"><span class="id" title="notation">}</span></a>.<br/> <br/> - <span class="id" title="keyword">Definition</span> <a name="d"><span class="id" title="definition">d</span></a> := (1<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#b3eea360671e1b32b18a26e15b3aace3"><span class="id" title="notation">+</span></a>2)%<span class="id" title="var">nat</span>.<br/> + <span class="id" title="keyword">Definition</span> <a name="d"><span class="id" title="definition">d</span></a> := (1<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a>2)%<span class="id" title="var">nat</span>.<br/> <br/> - <span class="id" title="keyword">Lemma</span> <a name="e"><span class="id" title="lemma">e</span></a> : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#3dcaec3b772747610227247939f96b01"><span class="id" title="notation">+</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> + <span class="id" title="keyword">Lemma</span> <a name="e"><span class="id" title="lemma">e</span></a> : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#e03f39daf98516fa530d3f6f5a1b4d92"><span class="id" title="notation">+</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> <span class="id" title="var">Admitted</span>.<br/> <br/> @@ -137,7 +137,7 @@ Various checks for coqdoc <span class="id" title="keyword">Variables</span> <a name="test2.test.b2"><span class="id" title="variable">b2</span></a>: <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> <br/> - <span class="id" title="keyword">Definition</span> <a name="a''"><span class="id" title="definition">a''</span></a> <span class="id" title="var">b</span> := <a class="idref" href="Coqdoc.links.html#test2.b'"><span class="id" title="variable">b'</span></a> <a class="idref" href="Coqdoc.links.html#1a1c7f13320341c3638e9edcc3e6389d"><span class="id" title="notation">++</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#O"><span class="id" title="constructor">O</span></a> <a class="idref" href="Coqdoc.links.html#1a1c7f13320341c3638e9edcc3e6389d"><span class="id" title="notation">++</span></a> <a class="idref" href="Coqdoc.links.html#test2.test.b2"><span class="id" title="variable">b2</span></a> <a class="idref" href="Coqdoc.links.html#347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">_</span></a> <a class="idref" href="Coqdoc.links.html#347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">++</span></a> <a class="idref" href="Coqdoc.links.html#347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">x</span></a> <a class="idref" href="Coqdoc.links.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#b3eea360671e1b32b18a26e15b3aace3"><span class="id" title="notation">+</span></a> <a class="idref" href="Coqdoc.links.html#h"><span class="id" title="abbreviation">h</span></a> 0.<br/> + <span class="id" title="keyword">Definition</span> <a name="a''"><span class="id" title="definition">a''</span></a> <span class="id" title="var">b</span> := <a class="idref" href="Coqdoc.links.html#test2.b'"><span class="id" title="variable">b'</span></a> <a class="idref" href="Coqdoc.links.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">++</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#O"><span class="id" title="constructor">O</span></a> <a class="idref" href="Coqdoc.links.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">++</span></a> <a class="idref" href="Coqdoc.links.html#test2.test.b2"><span class="id" title="variable">b2</span></a> <a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">_</span></a> <a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">++</span></a> <a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">x</span></a> <a class="idref" href="Coqdoc.links.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="Coqdoc.links.html#h"><span class="id" title="abbreviation">h</span></a> 0.<br/> <br/> <span class="id" title="keyword">End</span> <a class="idref" href="Coqdoc.links.html#test2.test"><span class="id" title="section">test</span></a>.<br/> diff --git a/test-suite/coqdoc/links.tex.out b/test-suite/coqdoc/links.tex.out index f42db99dc2..24f96ff1e6 100644 --- a/test-suite/coqdoc/links.tex.out +++ b/test-suite/coqdoc/links.tex.out @@ -51,34 +51,34 @@ Various checks for coqdoc \coqdockw{Definition} \coqdef{Coqdoc.links.f}{f}{\coqdocdefinition{f}} := \coqdockw{\ensuremath{\forall}} \coqdocvar{C}:\coqdockw{Prop}, \coqdocvariable{C}.\coqdoceol \coqdocemptyline \coqdocnoindent -\coqdockw{Notation} \coqdef{Coqdoc.links.::x '++' x}{"}{"}n ++ m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}).\coqdoceol +\coqdockw{Notation} \coqdef{Coqdoc.links.:::x '++' x}{"}{"}n ++ m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}).\coqdoceol \coqdocemptyline \coqdocnoindent -\coqdockw{Notation} \coqdef{Coqdoc.links.::x '++' x}{"}{"}n ++ m" := (\coqexternalref{mult}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{mult}} \coqdocvar{n} \coqdocvar{m}). \coqdocemptyline +\coqdockw{Notation} \coqdef{Coqdoc.links.:::x '++' x}{"}{"}n ++ m" := (\coqexternalref{mult}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{mult}} \coqdocvar{n} \coqdocvar{m}). \coqdocemptyline \coqdocnoindent -\coqdockw{Notation} \coqdef{Coqdoc.links.::x '**' x}{"}{"}n ** m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}) (\coqdoctac{at} \coqdockw{level} 60).\coqdoceol +\coqdockw{Notation} \coqdef{Coqdoc.links.:::x '**' x}{"}{"}n ** m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}) (\coqdoctac{at} \coqdockw{level} 60).\coqdoceol \coqdocemptyline \coqdocnoindent -\coqdockw{Notation} \coqdef{Coqdoc.links.::x 'xE2x96xB5' x}{"}{"}n ▵ m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}) (\coqdoctac{at} \coqdockw{level} 60).\coqdoceol +\coqdockw{Notation} \coqdef{Coqdoc.links.:::x 'xE2x96xB5' x}{"}{"}n ▵ m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}) (\coqdoctac{at} \coqdockw{level} 60).\coqdoceol \coqdocemptyline \coqdocnoindent -\coqdockw{Notation} \coqdef{Coqdoc.links.::x ''' ''' '++' 'x' x}{"}{"}n '\_' ++ 'x' m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}) (\coqdoctac{at} \coqdockw{level} 3).\coqdoceol +\coqdockw{Notation} \coqdef{Coqdoc.links.:::x ''' ''' '++' 'x' x}{"}{"}n '\_' ++ 'x' m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}) (\coqdoctac{at} \coqdockw{level} 3).\coqdoceol \coqdocemptyline \coqdocnoindent -\coqdockw{Inductive} \coqdef{Coqdoc.links.eq}{eq}{\coqdocinductive{eq}} (\coqdocvar{A}:\coqdockw{Type}) (\coqdocvar{x}:\coqdocvariable{A}) : \coqdocvar{A} \coqexternalref{:type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqdockw{Prop} := \coqdef{Coqdoc.links.eq refl}{eq\_refl}{\coqdocconstructor{eq\_refl}} : \coqdocvariable{x} \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{=}} \coqdocvariable{x} \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{:>}}\coqdocvariable{A}\coqdoceol +\coqdockw{Inductive} \coqdef{Coqdoc.links.eq}{eq}{\coqdocinductive{eq}} (\coqdocvar{A}:\coqdockw{Type}) (\coqdocvar{x}:\coqdocvariable{A}) : \coqdocvar{A} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqdockw{Prop} := \coqdef{Coqdoc.links.eq refl}{eq\_refl}{\coqdocconstructor{eq\_refl}} : \coqdocvariable{x} \coqref{Coqdoc.links.::type scope:x '=' x ':>' x}{\coqdocnotation{=}} \coqdocvariable{x} \coqref{Coqdoc.links.::type scope:x '=' x ':>' x}{\coqdocnotation{:>}}\coqdocvariable{A}\coqdoceol \coqdocnoindent \coqdoceol \coqdocnoindent -\coqdockw{where} \coqdef{Coqdoc.links.:type scope:x '=' x ':>' x}{"}{"}x = y :> A" := (@\coqref{Coqdoc.links.eq}{\coqdocinductive{eq}} \coqdocvar{A} \coqdocvar{x} \coqdocvar{y}) : \coqdocvar{type\_scope}.\coqdoceol +\coqdockw{where} \coqdef{Coqdoc.links.::type scope:x '=' x ':>' x}{"}{"}x = y :> A" := (@\coqref{Coqdoc.links.eq}{\coqdocinductive{eq}} \coqdocvar{A} \coqdocvar{x} \coqdocvar{y}) : \coqdocvar{type\_scope}.\coqdoceol \coqdocemptyline \coqdocnoindent -\coqdockw{Definition} \coqdef{Coqdoc.links.eq0}{eq0}{\coqdocdefinition{eq0}} := 0 \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{=}} 0 \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{:>}} \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol +\coqdockw{Definition} \coqdef{Coqdoc.links.eq0}{eq0}{\coqdocdefinition{eq0}} := 0 \coqref{Coqdoc.links.::type scope:x '=' x ':>' x}{\coqdocnotation{=}} 0 \coqref{Coqdoc.links.::type scope:x '=' x ':>' x}{\coqdocnotation{:>}} \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol \coqdocemptyline \coqdocnoindent -\coqdockw{Notation} \coqdef{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{"}{"}( x \# y ; .. ; z )" := (\coqexternalref{pair}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{pair}} .. (\coqexternalref{pair}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{pair}} \coqdocvar{x} \coqdocvar{y}) .. \coqdocvar{z}).\coqdoceol +\coqdockw{Notation} \coqdef{Coqdoc.links.:::'(' x 'x23' x ';' '..' ';' x ')'}{"}{"}( x \# y ; .. ; z )" := (\coqexternalref{pair}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{pair}} .. (\coqexternalref{pair}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{pair}} \coqdocvar{x} \coqdocvar{y}) .. \coqdocvar{z}).\coqdoceol \coqdocemptyline \coqdocnoindent -\coqdockw{Definition} \coqdef{Coqdoc.links.b xCExB1}{b\_α}{\coqdocdefinition{b\_α}} := \coqexternalref{:core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{(}}\coqref{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{(}}0\coqref{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{\#}}0\coqref{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{;}}0\coqref{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{)}} \coqexternalref{:core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{,}} \coqexternalref{:core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{(}}0 \coqref{Coqdoc.links.::x '**' x}{\coqdocnotation{**}} 0\coqexternalref{:core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{))}}.\coqdoceol +\coqdockw{Definition} \coqdef{Coqdoc.links.b xCExB1}{b\_α}{\coqdocdefinition{b\_α}} := \coqexternalref{::core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{(}}\coqref{Coqdoc.links.:::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{(}}0\coqref{Coqdoc.links.:::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{\#}}0\coqref{Coqdoc.links.:::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{;}}0\coqref{Coqdoc.links.:::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{)}} \coqexternalref{::core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{,}} \coqexternalref{::core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{(}}0 \coqref{Coqdoc.links.:::x '**' x}{\coqdocnotation{**}} 0\coqexternalref{::core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{))}}.\coqdoceol \coqdocemptyline \coqdocnoindent \coqdockw{Notation} \coqdef{Coqdoc.links.h}{h}{\coqdocabbreviation{h}} := \coqref{Coqdoc.links.a}{\coqdocdefinition{a}}.\coqdoceol @@ -90,7 +90,7 @@ Various checks for coqdoc \coqdockw{Variables} \coqdef{Coqdoc.links.test.b'}{b'}{\coqdocvariable{b'}} \coqdef{Coqdoc.links.test.b2}{b2}{\coqdocvariable{b2}}: \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol \coqdocemptyline \coqdocindent{2.00em} -\coqdockw{Notation} \coqdef{Coqdoc.links.test.:my scope:x '+' x}{"}{"}n + m" := (\coqdocvar{n} \coqref{Coqdoc.links.::x 'xE2x96xB5' x}{\coqdocnotation{▵}} \coqdocvar{m}) : \coqdocvar{my\_scope}.\coqdoceol +\coqdockw{Notation} \coqdef{Coqdoc.links.test.::my scope:x '+' x}{"}{"}n + m" := (\coqdocvar{n} \coqref{Coqdoc.links.:::x 'xE2x96xB5' x}{\coqdocnotation{▵}} \coqdocvar{m}) : \coqdocvar{my\_scope}.\coqdoceol \coqdocemptyline \coqdocindent{2.00em} \coqdockw{Delimit} \coqdockw{Scope} \coqdocvar{my\_scope} \coqdockw{with} \coqdocvar{my}.\coqdoceol @@ -99,19 +99,19 @@ Various checks for coqdoc \coqdockw{Notation} \coqdef{Coqdoc.links.l}{l}{\coqdocabbreviation{l}} := 0.\coqdoceol \coqdocemptyline \coqdocindent{2.00em} -\coqdockw{Definition} \coqdef{Coqdoc.links.xCExB1}{α}{\coqdocdefinition{α}} := (0 \coqref{Coqdoc.links.test.:my scope:x '+' x}{\coqdocnotation{+}} \coqref{Coqdoc.links.l}{\coqdocabbreviation{l}})\%\coqdocvar{my}.\coqdoceol +\coqdockw{Definition} \coqdef{Coqdoc.links.xCExB1}{α}{\coqdocdefinition{α}} := (0 \coqref{Coqdoc.links.test.::my scope:x '+' x}{\coqdocnotation{+}} \coqref{Coqdoc.links.l}{\coqdocabbreviation{l}})\%\coqdocvar{my}.\coqdoceol \coqdocemptyline \coqdocindent{2.00em} -\coqdockw{Definition} \coqdef{Coqdoc.links.a'}{a'}{\coqdocdefinition{a'}} \coqdocvar{b} := \coqdocvariable{b'}\coqref{Coqdoc.links.::x '++' x}{\coqdocnotation{++}}0\coqref{Coqdoc.links.::x '++' x}{\coqdocnotation{++}}\coqdocvariable{b2} \coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{\_}} \coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{++}}\coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{x}} \coqdocvariable{b}.\coqdoceol +\coqdockw{Definition} \coqdef{Coqdoc.links.a'}{a'}{\coqdocdefinition{a'}} \coqdocvar{b} := \coqdocvariable{b'}\coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}}0\coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}}\coqdocvariable{b2} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{\_}} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{++}}\coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{x}} \coqdocvariable{b}.\coqdoceol \coqdocemptyline \coqdocindent{2.00em} -\coqdockw{Definition} \coqdef{Coqdoc.links.c}{c}{\coqdocdefinition{c}} := \coqexternalref{:type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\{}}\coqexternalref{True}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocinductive{True}}\coqexternalref{:type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\}+\{}}\coqexternalref{True}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocinductive{True}}\coqexternalref{:type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\}}}.\coqdoceol +\coqdockw{Definition} \coqdef{Coqdoc.links.c}{c}{\coqdocdefinition{c}} := \coqexternalref{::type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\{}}\coqexternalref{True}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocinductive{True}}\coqexternalref{::type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\}+\{}}\coqexternalref{True}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocinductive{True}}\coqexternalref{::type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\}}}.\coqdoceol \coqdocemptyline \coqdocindent{2.00em} -\coqdockw{Definition} \coqdef{Coqdoc.links.d}{d}{\coqdocdefinition{d}} := (1\coqexternalref{:nat scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocnotation{+}}2)\%\coqdocvar{nat}.\coqdoceol +\coqdockw{Definition} \coqdef{Coqdoc.links.d}{d}{\coqdocdefinition{d}} := (1\coqexternalref{::nat scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocnotation{+}}2)\%\coqdocvar{nat}.\coqdoceol \coqdocemptyline \coqdocindent{2.00em} -\coqdockw{Lemma} \coqdef{Coqdoc.links.e}{e}{\coqdoclemma{e}} : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}} \coqexternalref{:type scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{+}} \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol +\coqdockw{Lemma} \coqdef{Coqdoc.links.e}{e}{\coqdoclemma{e}} : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}} \coqexternalref{::type scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{+}} \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol \coqdocindent{2.00em} \coqdocvar{Admitted}.\coqdoceol \coqdocemptyline @@ -131,7 +131,7 @@ Various checks for coqdoc \coqdockw{Variables} \coqdef{Coqdoc.links.test2.test.b2}{b2}{\coqdocvariable{b2}}: \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol \coqdocemptyline \coqdocindent{3.00em} -\coqdockw{Definition} \coqdef{Coqdoc.links.a''}{a'{}'}{\coqdocdefinition{a'{}'}} \coqdocvar{b} := \coqdocvariable{b'} \coqref{Coqdoc.links.::x '++' x}{\coqdocnotation{++}} \coqexternalref{O}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{O}} \coqref{Coqdoc.links.::x '++' x}{\coqdocnotation{++}} \coqdocvariable{b2} \coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{\_}} \coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{++}} \coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{x}} \coqdocvariable{b} \coqexternalref{:nat scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocnotation{+}} \coqref{Coqdoc.links.h}{\coqdocabbreviation{h}} 0.\coqdoceol +\coqdockw{Definition} \coqdef{Coqdoc.links.a''}{a'{}'}{\coqdocdefinition{a'{}'}} \coqdocvar{b} := \coqdocvariable{b'} \coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}} \coqexternalref{O}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{O}} \coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}} \coqdocvariable{b2} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{\_}} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{++}} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{x}} \coqdocvariable{b} \coqexternalref{::nat scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocnotation{+}} \coqref{Coqdoc.links.h}{\coqdocabbreviation{h}} 0.\coqdoceol \coqdocemptyline \coqdocindent{2.00em} \coqdockw{End} \coqref{Coqdoc.links.test2.test}{\coqdocsection{test}}.\coqdoceol diff --git a/test-suite/misc/7704.sh b/test-suite/misc/7704.sh new file mode 100755 index 0000000000..0ca2c97d24 --- /dev/null +++ b/test-suite/misc/7704.sh @@ -0,0 +1,7 @@ +#!/usr/bin/env bash + +set -e + +export PATH=$BIN:$PATH + +${coqtop#"$BIN"} -compile misc/aux7704.v diff --git a/test-suite/misc/aux7704.v b/test-suite/misc/aux7704.v new file mode 100644 index 0000000000..6fdcf67684 --- /dev/null +++ b/test-suite/misc/aux7704.v @@ -0,0 +1,6 @@ + +Goal True /\ True. +Proof. + split. + par:exact I. +Qed. diff --git a/test-suite/output/BadOptionValueType.out b/test-suite/output/BadOptionValueType.out new file mode 100644 index 0000000000..34d8518a75 --- /dev/null +++ b/test-suite/output/BadOptionValueType.out @@ -0,0 +1,8 @@ +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. +The command has indeed failed with message: +Bad type of value for this option: expected bool, got int. +The command has indeed failed with message: +Bad type of value for this option: expected bool, got int. diff --git a/test-suite/output/BadOptionValueType.v b/test-suite/output/BadOptionValueType.v new file mode 100644 index 0000000000..b61c3757ba --- /dev/null +++ b/test-suite/output/BadOptionValueType.v @@ -0,0 +1,4 @@ +Fail Set Default Timeout "2". +Fail Set Debug Eauto "yes". +Fail Set Debug Eauto 1. +Fail Set Implicit Arguments 1. diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 419dcadb4c..dfab400baa 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -169,3 +169,5 @@ fun x : K => match x with | _ => 2 end : K -> nat +The command has indeed failed with message: +Pattern "S _, _" is redundant in this clause. diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 4740c009a4..e4fa7044e7 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -217,3 +217,6 @@ Check fun x => match x with a3 | a4 => 3 | _ => 2 end. Check fun x => match x with a3 => 3 | a2 | a1 => 4 | _ => 2 end. Check fun x => match x with a4 => 3 | a2 | a1 => 4 | _ => 2 end. Check fun x => match x with a3 | a4 | a1 => 3 | _ => 2 end. + +(* Test redundant clause within a disjunctive pattern *) +Fail Check fun n m => match n, m with 0, 0 | _, S _ | S 0, _ | S (S _ | _), _ => false end. diff --git a/test-suite/output/Deprecation.out b/test-suite/output/Deprecation.out new file mode 100644 index 0000000000..7e290847c1 --- /dev/null +++ b/test-suite/output/Deprecation.out @@ -0,0 +1,3 @@ +File "stdin", line 5, characters 0-3: +Warning: Tactic foo is deprecated since X.Y. Use idtac instead. +[deprecated-tactic,deprecated] diff --git a/test-suite/output/Deprecation.v b/test-suite/output/Deprecation.v new file mode 100644 index 0000000000..04d5eb3d4a --- /dev/null +++ b/test-suite/output/Deprecation.v @@ -0,0 +1,6 @@ +#[deprecated(since = "X.Y", note = "Use idtac instead.")] + Ltac foo := idtac. + +Goal True. +foo. +Abort. diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 996af59270..d32cf67e28 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -241,3 +241,14 @@ Notation Notation "( x , y , .. , z )" := pair .. (pair x y) .. z : core_scope (default interpretation) +1 subgoal + + ============================ + ##@% + ^^^ +myfoo01 tt + : nat +myfoo01 tt + : nat +myfoo01 tt + : nat diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 3cf0c913f7..180e8d337e 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -385,3 +385,28 @@ Module LocateNotations. Locate "exists". Locate "( _ , _ , .. , _ )". End LocateNotations. + +Module Issue7731. + +Axiom (P : nat -> Prop). +Parameter (X : nat). +Notation "## @ E ^^^" := (P E) (at level 20, E at level 1, format "'[ ' ## '/' @ E '/' ^^^ ']'"). +Notation "%" := X. + +Set Printing Width 7. +Goal ## @ % ^^^. +Show. +Abort. + +End Issue7731. + +Module Issue8126. + +Definition myfoo (x : nat) (y : nat) (z : unit) := y. +Notation myfoo0 := (@myfoo 0). +Notation myfoo01 := (@myfoo0 1). +Check myfoo 0 1 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI] *) +Check myfoo0 1 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI] *) +Check myfoo01 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI] *) + +End Issue8126. diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out new file mode 100644 index 0000000000..cef7d1a702 --- /dev/null +++ b/test-suite/output/Notations4.out @@ -0,0 +1,17 @@ +[< 0 > + < 1 > * < 2 >] + : nat +[<< # 0 >>] + : option nat +[1 {f 1}] + : Expr +fun (x : nat) (y z : Expr) => [1 + y z + {f x}] + : nat -> Expr -> Expr -> Expr +fun e : Expr => +match e with +| [x y + z] => [x + y z] +| [1 + 1] => [1] +| _ => [e + e] +end + : Expr -> Expr +[(1 + 1)] + : Expr diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v new file mode 100644 index 0000000000..9738ce5a5e --- /dev/null +++ b/test-suite/output/Notations4.v @@ -0,0 +1,68 @@ +(* An example with constr subentries *) + +Module A. + +Declare Custom Entry myconstr. + +Notation "[ x ]" := x (x custom myconstr at level 6). +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 >]. + +Declare Custom Entry anotherconstr. + +Notation "[ x ]" := x (x custom myconstr at level 6). +Notation "<< x >>" := x (in custom myconstr at level 3, x custom anotherconstr at level 10). +Notation "# x" := (Some x) (in custom anotherconstr at level 8, x constr at level 9). +Check [ << # 0 >> ]. + +End A. + +Module B. + +Inductive Expr := + | Mul : Expr -> Expr -> Expr + | Add : Expr -> Expr -> Expr + | One : Expr. + +Declare Custom Entry expr. +Notation "[ expr ]" := expr (expr custom expr at level 2). +Notation "1" := One (in custom expr at level 0). +Notation "x y" := (Mul x y) (in custom expr at level 1, left associativity). +Notation "x + y" := (Add x y) (in custom expr at level 2, left associativity). +Notation "( x )" := x (in custom expr at level 0, x at level 2). +Notation "{ x }" := x (in custom expr at level 0, x constr). +Notation "x" := x (in custom expr at level 0, x ident). + +Axiom f : nat -> Expr. +Check [1 {f 1}]. +Check fun x y z => [1 + y z + {f x}]. +Check fun e => match e with +| [x y + z] => [x + y z] +| [1 + 1] => [1] +| y => [y + e] +end. + +End B. + +Module C. + +Inductive Expr := + | Add : Expr -> Expr -> Expr + | One : Expr. + +Declare Custom Entry expr. +Notation "[ expr ]" := expr (expr custom expr at level 1). +Notation "1" := One (in custom expr at level 0). +Notation "x + y" := (Add x y) (in custom expr at level 2, left associativity). +Notation "( x )" := x (in custom expr at level 0, x at level 2). + +(* Check the use of a two-steps coercion from constr to expr 1 then + from expr 0 to expr 2 (note that camlp5 parsing is more tolerant + and does not require parentheses to parse from level 2 while at + level 1) *) + +Check [1 + 1]. + +End C. diff --git a/test-suite/output/RecordMissingField.out b/test-suite/output/RecordMissingField.out new file mode 100644 index 0000000000..7c80a6065f --- /dev/null +++ b/test-suite/output/RecordMissingField.out @@ -0,0 +1,4 @@ +File "stdin", line 8, characters 5-22: +Error: Cannot infer field y2p of record point2d in environment: +p : point2d + diff --git a/test-suite/output/RecordMissingField.v b/test-suite/output/RecordMissingField.v new file mode 100644 index 0000000000..84f1748fa0 --- /dev/null +++ b/test-suite/output/RecordMissingField.v @@ -0,0 +1,8 @@ +(** Check for error message when missing a record field. Error message +should contain missing field, and the inferred type of the record **) + +Record point2d := mkPoint { x2p: nat; y2p: nat }. + + +Definition increment_x (p: point2d) : point2d := + {| x2p := x2p p + 1; |}. diff --git a/test-suite/output/ssr_explain_match.out b/test-suite/output/ssr_explain_match.out index fa2393b910..32cfb354bf 100644 --- a/test-suite/output/ssr_explain_match.out +++ b/test-suite/output/ssr_explain_match.out @@ -1,35 +1,35 @@ File "stdin", line 12, characters 0-61: -Warning: Notation _ - _ was already used in scope nat_scope. +Warning: Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing] File "stdin", line 12, characters 0-61: -Warning: Notation _ <= _ was already used in scope nat_scope. +Warning: Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "stdin", line 12, characters 0-61: -Warning: Notation _ < _ was already used in scope nat_scope. +Warning: Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "stdin", line 12, characters 0-61: -Warning: Notation _ >= _ was already used in scope nat_scope. +Warning: Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing] File "stdin", line 12, characters 0-61: -Warning: Notation _ > _ was already used in scope nat_scope. +Warning: Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing] File "stdin", line 12, characters 0-61: -Warning: Notation _ <= _ <= _ was already used in scope nat_scope. +Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "stdin", line 12, characters 0-61: -Warning: Notation _ < _ <= _ was already used in scope nat_scope. +Warning: Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "stdin", line 12, characters 0-61: -Warning: Notation _ <= _ < _ was already used in scope nat_scope. +Warning: Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "stdin", line 12, characters 0-61: -Warning: Notation _ < _ < _ was already used in scope nat_scope. +Warning: Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "stdin", line 12, characters 0-61: -Warning: Notation _ + _ was already used in scope nat_scope. +Warning: Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing] File "stdin", line 12, characters 0-61: -Warning: Notation _ * _ was already used in scope nat_scope. +Warning: Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing] BEGIN INSTANCES instance: (x + y + z) matches: (x + y + z) diff --git a/test-suite/success/ssr_delayed_clear_rename.v b/test-suite/ssr/delayed_clear_rename.v index 951e5aff79..951e5aff79 100644 --- a/test-suite/success/ssr_delayed_clear_rename.v +++ b/test-suite/ssr/delayed_clear_rename.v diff --git a/test-suite/ssr/rewrite_illtyped.v b/test-suite/ssr/rewrite_illtyped.v new file mode 100644 index 0000000000..7358068c8d --- /dev/null +++ b/test-suite/ssr/rewrite_illtyped.v @@ -0,0 +1,9 @@ +From Coq Require Import ssreflect Setoid. + +Structure SEProp := {prop_of : Prop; _ : prop_of <-> True}. + +Fact anomaly: forall P : SEProp, prop_of P. +Proof. +move=> [P E]. +Fail rewrite E. +Abort. diff --git a/test-suite/success/BracketsWithGoalSelector.v b/test-suite/success/BracketsWithGoalSelector.v index ed035f5213..2f7425bce6 100644 --- a/test-suite/success/BracketsWithGoalSelector.v +++ b/test-suite/success/BracketsWithGoalSelector.v @@ -14,3 +14,12 @@ Proof. Fail Qed. } Qed. + +Lemma foo (n: nat) (P : nat -> Prop): + P n. +Proof. + intros. + refine (nat_ind _ ?[Base] ?[Step] _). + [Base]: { admit. } + [Step]: { admit. } +Abort. diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v index 717dc0debe..ebf5b094e1 100644 --- a/test-suite/success/Hints.v +++ b/test-suite/success/Hints.v @@ -183,3 +183,33 @@ End HintCut. Goal forall (m : nat), exists n, m = n /\ m = n. intros m; eexists; split; [trivial | reflexivity]. Qed. + +Section HintTransparent. + + Definition fn (x : nat) := S x. + + Create HintDb trans. + + Hint Resolve eq_refl | (_ = _) : trans. + + (* No reduction *) + Hint Variables Opaque : trans. Hint Constants Opaque : trans. + + Goal forall x : nat, fn x = S x. + Proof. + intros. + Fail typeclasses eauto with trans. + unfold fn. + typeclasses eauto with trans. + Qed. + + (** Now allow unfolding fn *) + Hint Constants Transparent : trans. + + Goal forall x : nat, fn x = S x. + Proof. + intros. + typeclasses eauto with trans. + Qed. + +End HintTransparent. diff --git a/test-suite/success/Fourier.v b/test-suite/success/LraTest.v index b63bead477..bf3a87da25 100644 --- a/test-suite/success/Fourier.v +++ b/test-suite/success/LraTest.v @@ -1,12 +1,14 @@ -Require Import Rfunctions. -Require Import Fourier. +Require Import Reals. +Require Import Lra. + +Open Scope R_scope. Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z). -intros; split_Rabs; fourier. +intros; split_Rabs; lra. Qed. Lemma l2 : forall x y : R, x < Rabs y -> y < 1 -> x >= 0 -> - y <= 1 -> Rabs x <= 1. intros. -split_Rabs; fourier. +split_Rabs; lra. Qed. diff --git a/test-suite/success/LtacDeprecation.v b/test-suite/success/LtacDeprecation.v new file mode 100644 index 0000000000..633a5e4749 --- /dev/null +++ b/test-suite/success/LtacDeprecation.v @@ -0,0 +1,32 @@ +Set Warnings "+deprecated". + +#[deprecated(since = "8.8", note = "Use idtac instead")] +Ltac foo x := idtac. + +Goal True. +Fail (foo true). +Abort. + +Fail Ltac bar := foo. +Fail Tactic Notation "bar" := foo. + +#[deprecated(since = "8.8", note = "Use idtac instead")] +Tactic Notation "bar" := idtac. + +Goal True. +Fail bar. +Abort. + +Fail Ltac zar := bar. + +Set Warnings "-deprecated". + +Ltac zar := foo. +Ltac zarzar := bar. + +Set Warnings "+deprecated". + +Goal True. +zar x. +zarzar. +Abort. diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v index 7c2cf3ee52..1b33863e3b 100644 --- a/test-suite/success/Notations2.v +++ b/test-suite/success/Notations2.v @@ -126,3 +126,31 @@ Notation "'myexists' x , p" := (ex (fun x => p)) (at level 200, x ident, p at level 200, right associativity) : type_scope. Check myexists I, I = 0. (* Should not be seen as a constructor *) End M14. + +(* 15. Testing different ways to give the same levels without failing *) + +Module M15. + Local Notation "###### x" := (S x) (right associativity, at level 79, x at next level). + Fail Local Notation "###### x" := (S x) (right associativity, at level 79). + Local Notation "###### x" := (S x) (at level 79). +End M15. + +(* 16. Some test about custom entries *) +Module M16. + (* Test locality *) + Local Declare Custom Entry foo. + Fail Notation "#" := 0 (in custom foo). (* Should be local *) + Local Notation "#" := 0 (in custom foo). + + (* Test import *) + Module A. + Declare Custom Entry foo2. + End A. + Fail Notation "##" := 0 (in custom foo2). + Import A. + Local Notation "##" := 0 (in custom foo2). + + (* Test Print Grammar *) + Print Grammar foo. + Print Grammar foo2. +End M16. diff --git a/test-suite/success/attribute-syntax.v b/test-suite/success/attribute-syntax.v new file mode 100644 index 0000000000..83fb3d0c8e --- /dev/null +++ b/test-suite/success/attribute-syntax.v @@ -0,0 +1,23 @@ +From Coq Require Program. + +Section Scope. + +#[local] Coercion nat_of_bool (b: bool) : nat := + if b then 0 else 1. + +Check (refl_equal : true = 0 :> nat). + +End Scope. + +Fail Check 0 = true :> nat. + +#[polymorphic] +Definition ι T (x: T) := x. + +Check ι _ ι. + +#[program] +Fixpoint f (n: nat) {wf lt n} : nat := _. + +#[deprecated(since="8.9.0")] +Ltac foo := foo. diff --git a/test-suite/success/mutual_record.v b/test-suite/success/mutual_record.v new file mode 100644 index 0000000000..77529733be --- /dev/null +++ b/test-suite/success/mutual_record.v @@ -0,0 +1,57 @@ +Module M0. + +Inductive foo (A : Type) := Foo { + foo0 : option (bar A); + foo1 : nat; + foo2 := foo1 = 0; + foo3 : foo2; +} + +with bar (A : Type) := Bar { + bar0 : A; + bar1 := 0; + bar2 : bar1 = 0; + bar3 : nat -> foo A; +}. + +End M0. + +Module M1. + +Set Primitive Projections. + +Inductive foo (A : Type) := Foo { + foo0 : option (bar A); + foo1 : nat; + foo2 := foo1 = 0; + foo3 : foo2; +} + +with bar (A : Type) := Bar { + bar0 : A; + bar1 := 0; + bar2 : bar1 = 0; + bar3 : nat -> foo A; +}. + +End M1. + +Module M2. + +Set Primitive Projections. + +CoInductive foo (A : Type) := Foo { + foo0 : option (bar A); + foo1 : nat; + foo2 := foo1 = 0; + foo3 : foo2; +} + +with bar (A : Type) := Bar { + bar0 : A; + bar1 := 0; + bar2 : bar1 = 0; + bar3 : nat -> foo A; +}. + +End M2. diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v index 7ca2767a53..299b08bdd1 100644 --- a/test-suite/success/primitiveproj.v +++ b/test-suite/success/primitiveproj.v @@ -193,12 +193,13 @@ Set Primitive Projections. Record s (x:nat) (y:=S x) := {c:=x; d:x=c}. Lemma f : 0=1. Proof. -Fail apply d. + Fail apply d. (* split. reflexivity. Qed. *) +Abort. (* Primitive projection match compilation *) Require Import List. @@ -220,3 +221,9 @@ Fixpoint split_at {A} (l : list A) (n : nat) : prod (list A) (list A) := Time Eval vm_compute in split_at (repeat 0 20) 10. (* Takes 0s *) Time Eval vm_compute in split_at (repeat 0 40) 20. (* Takes 0.001s *) Timeout 1 Time Eval vm_compute in split_at (repeat 0 60) 30. (* Used to take 60s, now takes 0.001s *) + +Check (@eq_refl _ 0 <: 0 = fst (pair 0 1)). +Fail Check (@eq_refl _ 0 <: 0 = snd (pair 0 1)). + +Check (@eq_refl _ 0 <<: 0 = fst (pair 0 1)). +Fail Check (@eq_refl _ 0 <<: 0 = snd (pair 0 1)). diff --git a/test-suite/success/uniform_inductive_parameters.v b/test-suite/success/uniform_inductive_parameters.v new file mode 100644 index 0000000000..42236a5313 --- /dev/null +++ b/test-suite/success/uniform_inductive_parameters.v @@ -0,0 +1,13 @@ +Set Uniform Inductive Parameters. + +Inductive list (A : Type) := + | nil : list + | cons : A -> list -> list. +Check (list : Type -> Type). +Check (cons : forall A, A -> list A -> list A). + +Inductive list2 (A : Type) (A' := prod A A) := + | nil2 : list2 + | cons2 : A' -> list2 -> list2. +Check (list2 : Type -> Type). +Check (cons2 : forall A (A' := prod A A), A' -> list2 A -> list2 A). diff --git a/test-suite/success/vm_records.v b/test-suite/success/vm_records.v new file mode 100644 index 0000000000..8a1544c8ea --- /dev/null +++ b/test-suite/success/vm_records.v @@ -0,0 +1,40 @@ +Set Primitive Projections. + +Module M. + +CoInductive foo := Foo { + foo0 : foo; + foo1 : bar; +} +with bar := Bar { + bar0 : foo; + bar1 : bar; +}. + +CoFixpoint f : foo := Foo f g +with g : bar := Bar f g. + +Check (@eq_refl _ g.(bar0) <: f.(foo0).(foo0) = g.(bar0)). +Check (@eq_refl _ g <: g.(bar1).(bar0).(foo1) = g). + +End M. + +Module N. + +Inductive foo := Foo { + foo0 : option foo; + foo1 : list bar; +} +with bar := Bar { + bar0 : option bar; + bar1 : list foo; +}. + +Definition f_0 := Foo None nil. +Definition g_0 := Bar None nil. + +Definition f := Foo (Some f_0) (cons g_0 nil). + +Check (@eq_refl _ f.(foo1) <: f.(foo1) = cons g_0 nil). + +End N. diff --git a/test-suite/unit-tests/.merlin b/test-suite/unit-tests/.merlin.in index b2279de74e..b2279de74e 100644 --- a/test-suite/unit-tests/.merlin +++ b/test-suite/unit-tests/.merlin.in diff --git a/test-suite/unit-tests/clib/inteq.ml b/test-suite/unit-tests/clib/inteq.ml index c07ec293f0..89717c79d5 100644 --- a/test-suite/unit-tests/clib/inteq.ml +++ b/test-suite/unit-tests/clib/inteq.ml @@ -1,5 +1,7 @@ open Utest +let log_out_ch = open_log_out_ch __FILE__ + let eq0 = mk_bool_test "clib-inteq0" "Int.equal on 0" (Int.equal 0 0) @@ -10,4 +12,4 @@ let eq42 = mk_bool_test "clib-inteq42" let tests = [ eq0; eq42 ] -let _ = run_tests __FILE__ tests +let _ = run_tests __FILE__ log_out_ch tests diff --git a/test-suite/unit-tests/clib/unicode_tests.ml b/test-suite/unit-tests/clib/unicode_tests.ml index 9ae405977b..95316ad3aa 100644 --- a/test-suite/unit-tests/clib/unicode_tests.ml +++ b/test-suite/unit-tests/clib/unicode_tests.ml @@ -1,5 +1,7 @@ open Utest +let log_out_ch = open_log_out_ch __FILE__ + let unicode0 = mk_eq_test "clib-unicode0" "split_at_first_letter, first letter is character" None @@ -12,4 +14,4 @@ let unicode1 = mk_eq_test "clib-unicode1" let tests = [ unicode0; unicode1 ] -let _ = run_tests __FILE__ tests +let _ = run_tests __FILE__ log_out_ch tests diff --git a/test-suite/unit-tests/printing/proof_diffs_test.ml b/test-suite/unit-tests/printing/proof_diffs_test.ml new file mode 100644 index 0000000000..526cefec44 --- /dev/null +++ b/test-suite/unit-tests/printing/proof_diffs_test.ml @@ -0,0 +1,333 @@ +open OUnit +open Utest +open Pp_diff +open Proof_diffs + +let tokenize_string = Proof_diffs.tokenize_string +let diff_pp = diff_pp ~tokenize_string +let diff_str = diff_str ~tokenize_string + +let tests = ref [] +let add_test name test = tests := (mk_test name (TestCase test)) :: !tests + +let log_out_ch = open_log_out_ch __FILE__ +let cfprintf oc = Printf.(kfprintf (fun oc -> fprintf oc "") oc) +let cprintf s = cfprintf log_out_ch s +let _ = Proof_diffs.log_out_ch := log_out_ch + +let string_of_string s : string = "\"" ^ s ^ "\"" + +(* todo: OCaml: why can't the body of the test function be given in the add_test line? *) + +let t () = + let expected : diff_list = [] in + let diffs = diff_str "" " " in + + assert_equal ~msg:"empty" ~printer:string_of_diffs expected diffs; + let (has_added, has_removed) = has_changes diffs in + assert_equal ~msg:"has `Added" ~printer:string_of_bool false has_added; + assert_equal ~msg:"has `Removed" ~printer:string_of_bool false has_removed +let _ = add_test "diff_str empty" t + + +let t () = + let expected : diff_list = + [ `Common (0, 0, "a"); `Common (1, 1, "b"); `Common (2, 2, "c")] in + let diffs = diff_str "a b c" " a b\t c\n" in + + assert_equal ~msg:"white space" ~printer:string_of_diffs expected diffs; + let (has_added, has_removed) = has_changes diffs in + assert_equal ~msg:"no `Added" ~printer:string_of_bool false has_added; + assert_equal ~msg:"no `Removed" ~printer:string_of_bool false has_removed +let _ = add_test "diff_str white space" t + +let t () = + let expected : diff_list = [ `Removed (0, "a"); `Added (0, "b")] in + let diffs = diff_str "a" "b" in + + assert_equal ~msg:"add/remove" ~printer:string_of_diffs expected diffs; + let (has_added, has_removed) = has_changes diffs in + assert_equal ~msg:"has `Added" ~printer:string_of_bool true has_added; + 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 + *) +let t () = + List.iter (fun x -> cprintf "'%s' " x) (tokenize_string "(* comment *) \"string\" 'c' xx"); + cprintf "\n" +let _ = add_test "tokenize_string examples" t + +open Pp + +(* note pp_to_string concatenates adjacent strings, could become one token, +e.g. str " a" ++ str "b " will give a token "ab" *) +(* checks background is present and correct *) +let t () = + let o_pp = str "a" ++ str "!" ++ str "c" in + let n_pp = str "a" ++ str "?" ++ str "c" in + let (o_exp, n_exp) = (wrap_in_bg "diff.removed" (str "a" ++ (tag "diff.removed" (str "!")) ++ str "c"), + wrap_in_bg "diff.added" (str "a" ++ (tag "diff.added" (str "?")) ++ str "c")) in + let (o_diff, n_diff) = diff_pp o_pp n_pp in + + assert_equal ~msg:"removed" ~printer:db_string_of_pp o_exp o_diff; + assert_equal ~msg:"added" ~printer:db_string_of_pp n_exp n_diff +let _ = add_test "diff_pp/add_diff_tags add/remove" t + +let t () = + (*Printf.printf "%s\n" (string_of_diffs (diff_str "a d" "a b c d"));*) + let o_pp = str "a" ++ str " d" in + let n_pp = str "a" ++ str " b " ++ str " c " ++ str "d" ++ str " e " in + let n_exp = flatten (wrap_in_bg "diff.added" (seq [ + str "a"; + str " "; (tag "start.diff.added" (str "b ")); + (tag "end.diff.added" (str " c")); str " "; + (str "d"); + str " "; (tag "diff.added" (str "e")); str " " + ])) in + let (_, n_diff) = diff_pp o_pp n_pp in + + assert_equal ~msg:"added" ~printer:db_string_of_pp n_exp (flatten n_diff);; +let _ = add_test "diff_pp/add_diff_tags a span with spaces" t + + +let t () = + let o_pp = str " " in + let n_pp = tag "sometag" (str "a") in + let n_exp = flatten (wrap_in_bg "diff.added" (tag "diff.added" (tag "sometag" (str "a")))) in + let (_, n_diff) = diff_pp o_pp n_pp in + + assert_equal ~msg:"added" ~printer:db_string_of_pp n_exp (flatten n_diff) +let _ = add_test "diff_pp/add_diff_tags diff tags outside existing tags" t + +let t () = + let o_pp = str " " in + let n_pp = seq [(tag "sometag" (str " a ")); str "b"] in + let n_exp = flatten (wrap_in_bg "diff.added" + (seq [tag "sometag" (str " "); (tag "start.diff.added" (tag "sometag" (str "a "))); + (tag "end.diff.added" (str "b"))]) ) in + let (_, n_diff) = diff_pp o_pp n_pp in + + assert_equal ~msg:"added" ~printer:db_string_of_pp n_exp (flatten n_diff) +let _ = add_test "diff_pp/add_diff_tags existing tagged values with spaces" t + +let t () = + let o_pp = str " " in + let n_pp = str " a b " in + let n_exp = flatten (wrap_in_bg "diff.added" + (seq [str " "; tag "diff.added" (str "a b"); str " "])) in + let (_, n_diff) = diff_pp o_pp n_pp in + + assert_equal ~msg:"added" ~printer:db_string_of_pp n_exp (flatten n_diff) +let _ = add_test "diff_pp/add_diff_tags multiple tokens in pp" t + +let t () = + let o_pp = str "a d" in + let n_pp = seq [str "a b"; str "c d"] in + let n_exp = flatten (wrap_in_bg "diff.added" + (seq [str "a "; tag "start.diff.added" (str "b"); + tag "end.diff.added" (str "c"); str " d"])) in + let (_, n_diff) = diff_pp o_pp n_pp in + + assert_equal ~msg:"added" ~printer:db_string_of_pp n_exp (flatten n_diff) +let _ = add_test "diff_pp/add_diff_tags token spanning multiple Ppcmd_strs" t + +let t () = + let o_pp = seq [str ""; str "a"] in + let n_pp = seq [str ""; str "a b"] in + let n_exp = flatten (wrap_in_bg "diff.added" + (seq [str ""; str "a "; tag "diff.added" (str "b")])) in + let (_, n_diff) = diff_pp o_pp n_pp in + + assert_equal ~msg:"added" ~printer:db_string_of_pp n_exp (flatten n_diff) +let _ = add_test "diff_pp/add_diff_tags empty string preserved" t + +(* todo: awaiting a change in the lexer to return the quotes of the string token *) +let t () = + let s = "\"a b\"" in + let o_pp = seq [str s] in + let n_pp = seq [str "\"a b\" "] in + cprintf "ppcmds: %s\n" (string_of_ppcmds n_pp); + let n_exp = flatten (wrap_in_bg "diff.added" + (seq [str ""; str "a "; tag "diff.added" (str "b")])) in + let (_, n_diff) = diff_pp o_pp n_pp in + + assert_equal ~msg:"string" ~printer:string_of_string "a b" (List.hd (tokenize_string s)); + assert_equal ~msg:"added" ~printer:db_string_of_pp n_exp (flatten n_diff) +let _ = if false then add_test "diff_pp/add_diff_tags token containing white space" t + +let add_entries map idents rhs_pp = + let make_entry() = { idents; rhs_pp; done_ = false } in + List.iter (fun ident -> map := (StringMap.add ident (make_entry ()) !map); ()) idents;; + +let print_list hyps = List.iter (fun x -> cprintf "%s\n" (string_of_ppcmds (flatten x))) hyps +let db_print_list hyps = List.iter (fun x -> cprintf "%s\n" (db_string_of_pp (flatten x))) hyps + + +(* a : foo + b : bar car -> + b : car + a : foo bar *) +let t () = + write_diffs_option "removed"; (* turn on "removed" option *) + let o_line_idents = [ ["a"]; ["b"]] in + let o_hyp_map = ref StringMap.empty in + add_entries o_hyp_map ["a"] (str " : foo"); + add_entries o_hyp_map ["b"] (str " : bar car"); + let n_line_idents = [ ["b"]; ["a"]] in + let n_hyp_map = ref StringMap.empty in + add_entries n_hyp_map ["b"] (str " : car"); + add_entries n_hyp_map ["a"] (str " : foo bar"); + let expected = [flatten (wrap_in_bg "diff.removed" (seq [str "b"; str " : "; (tag "diff.removed" (str "bar")); str " car" ])); + flatten (wrap_in_bg "diff.added" (seq [str "b"; str " : car" ])); + flatten (wrap_in_bg "diff.added" (seq [str "a"; str " : foo "; (tag "diff.added" (str "bar")) ])) + ] in + + let hyps_diff_list = diff_hyps o_line_idents !o_hyp_map n_line_idents !n_hyp_map in + + (*print_list hyps_diff_list;*) + (*db_print_list hyps_diff_list;*) + + List.iter2 (fun exp act -> + assert_equal ~msg:"added" ~printer:db_string_of_pp exp (flatten act)) + expected hyps_diff_list +let _ = add_test "diff_hyps simple diffs" t + +(* a : nat + c, d : int -> + a, b : nat + d : int + and keeps old order *) +let t () = + write_diffs_option "removed"; (* turn on "removed" option *) + let o_line_idents = [ ["a"]; ["c"; "d"]] in + let o_hyp_map = ref StringMap.empty in + add_entries o_hyp_map ["a"] (str " : nat"); + add_entries o_hyp_map ["c"; "d"] (str " : int"); + let n_line_idents = [ ["a"; "b"]; ["d"]] in + let n_hyp_map = ref StringMap.empty in + add_entries n_hyp_map ["a"; "b"] (str " : nat"); + add_entries n_hyp_map ["d"] (str " : int"); + let expected = [flatten (wrap_in_bg "diff.added" (seq [str "a"; (tag "start.diff.added" (str ", ")); (tag "end.diff.added" (str "b")); str " : nat" ])); + flatten (wrap_in_bg "diff.removed" (seq [(tag "start.diff.removed" (str "c")); (tag "end.diff.removed" (str ",")); str " "; str "d"; str " : int" ])); + flatten (wrap_in_bg "diff.added" (seq [str "d"; str " : int" ])) + ] in + + let hyps_diff_list = diff_hyps o_line_idents !o_hyp_map n_line_idents !n_hyp_map in + + (*print_list hyps_diff_list;*) + (*print_list expected;*) + + (*db_print_list hyps_diff_list;*) + (*db_print_list expected;*) + + List.iter2 (fun exp act -> + assert_equal ~msg:"added" ~printer:db_string_of_pp exp (flatten act)) + expected hyps_diff_list +let _ = add_test "diff_hyps compacted" t + +(* a : foo + b : bar + c : nat -> + b, a, c : nat +DIFFS + b : bar (remove bar) + b : nat (add nat) + a : foo (remove foo) + a : nat (add nat) + c : nat + is this a realistic use case? +*) +let t () = + write_diffs_option "removed"; (* turn on "removed" option *) + let o_line_idents = [ ["a"]; ["b"]; ["c"]] in + let o_hyp_map = ref StringMap.empty in + add_entries o_hyp_map ["a"] (str " : foo"); + add_entries o_hyp_map ["b"] (str " : bar"); + add_entries o_hyp_map ["c"] (str " : nat"); + let n_line_idents = [ ["b"; "a"; "c"] ] in + let n_hyp_map = ref StringMap.empty in + add_entries n_hyp_map ["b"; "a"; "c"] (str " : nat"); + let expected = [flatten (wrap_in_bg "diff.removed" (seq [str "b"; str " : "; (tag "diff.removed" (str "bar"))])); + flatten (wrap_in_bg "diff.added" (seq [str "b"; str " : "; (tag "diff.added" (str "nat"))])); + flatten (wrap_in_bg "diff.removed" (seq [str "a"; str " : "; (tag "diff.removed" (str "foo"))])); + flatten (wrap_in_bg "diff.added" (seq [str "a"; str " : "; (tag "diff.added" (str "nat"))])); + flatten (seq [str "c"; str " : nat"]) + ] in + + let hyps_diff_list = diff_hyps o_line_idents !o_hyp_map n_line_idents !n_hyp_map in + + (*print_list hyps_diff_list;*) + (*db_print_list hyps_diff_list;*) + + List.iter2 (fun exp act -> + assert_equal ~msg:"added" ~printer:db_string_of_pp exp (flatten act)) + expected hyps_diff_list +let _ = add_test "diff_hyps compacted with join" t + +(* b, a, c : nat -> + a : foo + b : bar + c : nat +DIFFS + a : nat (remove nat) + a : foo (add foo) + b : nat (remove nat) + b : bar (add bar) + c : nat + is this a realistic use case? *) +let t () = + write_diffs_option "removed"; (* turn on "removed" option *) + let o_line_idents = [ ["b"; "a"; "c"] ] in + let o_hyp_map = ref StringMap.empty in + add_entries o_hyp_map ["b"; "a"; "c"] (str " : nat"); + let n_line_idents = [ ["a"]; ["b"]; ["c"]] in + let n_hyp_map = ref StringMap.empty in + add_entries n_hyp_map ["a"] (str " : foo"); + add_entries n_hyp_map ["b"] (str " : bar"); + add_entries n_hyp_map ["c"] (str " : nat"); + let expected = [flatten (wrap_in_bg "diff.removed" (seq [str "a"; str " : "; (tag "diff.removed" (str "nat"))])); + flatten (wrap_in_bg "diff.added" (seq [str "a"; str " : "; (tag "diff.added" (str "foo"))])); + flatten (wrap_in_bg "diff.removed" (seq [str "b"; str " : "; (tag "diff.removed" (str "nat"))])); + flatten (wrap_in_bg "diff.added" (seq [str "b"; str " : "; (tag "diff.added" (str "bar"))])); + flatten (seq [str "c"; str " : nat"]) + ] in + + let hyps_diff_list = diff_hyps o_line_idents !o_hyp_map n_line_idents !n_hyp_map in + + (*print_list hyps_diff_list;*) + (*db_print_list hyps_diff_list;*) + + List.iter2 (fun exp act -> + assert_equal ~msg:"added" ~printer:db_string_of_pp exp (flatten act)) + expected hyps_diff_list +let _ = add_test "diff_hyps compacted with split" t + + +(* other potential tests +coqtop/terminal formatting BLOCKED: CAN'T GET TAGS IN FORMATTER + white space at end of line + spanning diffs +shorten_diff_span + +MAYBE NOT WORTH IT +diff_pp/add_diff_tags + add/remove - show it preserves, recurs and processes: + nested in boxes + breaks, etc. preserved +diff_pp_combined with/without removed +*) + + +let _ = run_tests __FILE__ log_out_ch (List.rev !tests) diff --git a/test-suite/unit-tests/src/utest.ml b/test-suite/unit-tests/src/utest.ml index 069e6a4bf3..0cb1780ec9 100644 --- a/test-suite/unit-tests/src/utest.ml +++ b/test-suite/unit-tests/src/utest.ml @@ -42,10 +42,12 @@ let run_one logit test = let results = perform_test (fun _ -> ()) test in process_results results -(* run list of OUnit test cases, log results *) -let run_tests ml_fn tests = +let open_log_out_ch ml_fn = let log_fn = ml_fn ^ ".log" in - let out_ch = open_out log_fn in + open_out log_fn + +(* run list of OUnit test cases, log results *) +let run_tests ml_fn out_ch tests = let cprintf s = cfprintf out_ch s in let ceprintf s = cfprintf stderr s in let logit = logger out_ch in diff --git a/test-suite/unit-tests/src/utest.mli b/test-suite/unit-tests/src/utest.mli index 70928228bf..2e0f26e96b 100644 --- a/test-suite/unit-tests/src/utest.mli +++ b/test-suite/unit-tests/src/utest.mli @@ -9,4 +9,10 @@ val mk_bool_test : string -> string -> bool -> OUnit.test (* the string argument should be the name of the .ml file containing the tests; use __FILE__ for that purpose. *) -val run_tests : string -> OUnit.test list -> unit +val run_tests : string -> out_channel -> OUnit.test list -> unit + +(** open output channel for the test log file *) +(* the string argument should be the name of the .ml file + containing the tests; use __FILE__ for that purpose. + *) +val open_log_out_ch : string -> out_channel |