diff options
Diffstat (limited to 'test-suite')
34 files changed, 171 insertions, 35 deletions
diff --git a/test-suite/bugs/closed/bug_8785.v b/test-suite/bugs/closed/bug_8785.v new file mode 100644 index 0000000000..b10569499e --- /dev/null +++ b/test-suite/bugs/closed/bug_8785.v @@ -0,0 +1,44 @@ +Universe u v w. +Inductive invertible {X:Type@{u}} {Y:Type} (f:X->Y) : Prop := . + +Inductive FiniteT : Type -> Prop := + | add_finite: forall T:Type@{v}, FiniteT T -> FiniteT (option T) + | bij_finite: forall (X:Type@{w}) (Y:Type) (f:X->Y), FiniteT X -> + invertible f -> FiniteT Y. + +Set Printing Universes. + +Axiom a : False. +(* +Constraint v <= u. +Constraint v <= w. +*) +Lemma finite_subtype: forall (X:Type) (P:X->Prop), + FiniteT X -> (forall x:X, P x \/ ~ P x) -> + FiniteT {x:X | P x}. +Proof. +intros. +induction H. + +destruct (H0 None). +elim a. + +pose (g := fun (x:{x:T | P (Some x)}) => + match x return {x:option T | P x} with + | exist _ x0 i => exist (fun x:option T => P x) (Some x0) i + end). +apply bij_finite with _ g. +apply IHFiniteT. +intro; apply H0. +elim a. + +pose (g := fun (x:{x:X | P (f x)}) => + match x with + | exist _ x0 i => exist (fun x:Y => P x) (f x0) i + end). +apply bij_finite with _ g. +apply IHFiniteT. +intro; apply H0. +elim a. + +Qed. diff --git a/test-suite/bugs/closed/bug_8794.v b/test-suite/bugs/closed/bug_8794.v new file mode 100644 index 0000000000..5ff0b30260 --- /dev/null +++ b/test-suite/bugs/closed/bug_8794.v @@ -0,0 +1,11 @@ +(* This used to raise an anomaly in 8.8 *) + +Inductive T := Tau (t : T). + +Notation idT t := (match t with Tau t => Tau t end). + +Lemma match_itree : forall (t : T), t = idT t. +Proof. destruct t; auto. Qed. + +Lemma what (k : unit -> T) : k tt = k tt. +Proof. rewrite match_itree. Abort. diff --git a/test-suite/bugs/closed/bug_8848.v b/test-suite/bugs/closed/bug_8848.v new file mode 100644 index 0000000000..26563e6747 --- /dev/null +++ b/test-suite/bugs/closed/bug_8848.v @@ -0,0 +1,18 @@ +Require Import Program. +Set Implicit Arguments. +Unset Strict Implicit. + +Definition def (a : nat) := a = a. + +Structure record {a : nat} {D : def a} := + inR { prop : Prop }. + +Program +Canonical Structure ins (a : nat) (rec : @record a _) := + @inR a _ (prop rec). +Next Obligation. + exact eq_refl. +Defined. +Next Obligation. + exact eq_refl. +Defined. diff --git a/test-suite/coq-makefile/arg/_CoqProject b/test-suite/coq-makefile/arg/_CoqProject index 53dc963997..ed31a58247 100644 --- a/test-suite/coq-makefile/arg/_CoqProject +++ b/test-suite/coq-makefile/arg/_CoqProject @@ -4,7 +4,7 @@ -arg "-w default" src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/compat-subdirs/_CoqProject b/test-suite/coq-makefile/compat-subdirs/_CoqProject index 4f44bde22a..1f914a71b0 100644 --- a/test-suite/coq-makefile/compat-subdirs/_CoqProject +++ b/test-suite/coq-makefile/compat-subdirs/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/coqdoc1/_CoqProject b/test-suite/coq-makefile/coqdoc1/_CoqProject index 35792066bb..aa9473eaf0 100644 --- a/test-suite/coq-makefile/coqdoc1/_CoqProject +++ b/test-suite/coq-makefile/coqdoc1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/coqdoc2/_CoqProject b/test-suite/coq-makefile/coqdoc2/_CoqProject index d2a547d47b..0068554d72 100644 --- a/test-suite/coq-makefile/coqdoc2/_CoqProject +++ b/test-suite/coq-makefile/coqdoc2/_CoqProject @@ -3,7 +3,7 @@ -I src/ src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/emptyprefix/_CoqProject b/test-suite/coq-makefile/emptyprefix/_CoqProject index 5678a8edbb..3133342f6c 100644 --- a/test-suite/coq-makefile/emptyprefix/_CoqProject +++ b/test-suite/coq-makefile/emptyprefix/_CoqProject @@ -4,7 +4,7 @@ -arg "-w default" src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/extend-subdirs/_CoqProject b/test-suite/coq-makefile/extend-subdirs/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/extend-subdirs/_CoqProject +++ b/test-suite/coq-makefile/extend-subdirs/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/findlib-package/_CoqProject b/test-suite/coq-makefile/findlib-package/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/findlib-package/_CoqProject +++ b/test-suite/coq-makefile/findlib-package/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/latex1/_CoqProject b/test-suite/coq-makefile/latex1/_CoqProject index 35792066bb..aa9473eaf0 100644 --- a/test-suite/coq-makefile/latex1/_CoqProject +++ b/test-suite/coq-makefile/latex1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/merlin1/_CoqProject b/test-suite/coq-makefile/merlin1/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/merlin1/_CoqProject +++ b/test-suite/coq-makefile/merlin1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/mlpack1/_CoqProject b/test-suite/coq-makefile/mlpack1/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/mlpack1/_CoqProject +++ b/test-suite/coq-makefile/mlpack1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/mlpack2/_CoqProject b/test-suite/coq-makefile/mlpack2/_CoqProject index 51864a87ae..3db54e0a0b 100644 --- a/test-suite/coq-makefile/mlpack2/_CoqProject +++ b/test-suite/coq-makefile/mlpack2/_CoqProject @@ -3,7 +3,7 @@ -I src/ src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/multiroot/_CoqProject b/test-suite/coq-makefile/multiroot/_CoqProject index b384bb6d97..f53eef99a8 100644 --- a/test-suite/coq-makefile/multiroot/_CoqProject +++ b/test-suite/coq-makefile/multiroot/_CoqProject @@ -4,7 +4,7 @@ -I src/ ./src/test_plugin.mllib -./src/test.ml4 +./src/test.mlg ./src/test.mli ./src/test_aux.ml ./src/test_aux.mli diff --git a/test-suite/coq-makefile/native1/_CoqProject b/test-suite/coq-makefile/native1/_CoqProject index a6fa17348c..847b2c00a9 100644 --- a/test-suite/coq-makefile/native1/_CoqProject +++ b/test-suite/coq-makefile/native1/_CoqProject @@ -4,7 +4,7 @@ -arg -native-compiler src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/only/_CoqProject b/test-suite/coq-makefile/only/_CoqProject index 357384fddf..619a8fa459 100644 --- a/test-suite/coq-makefile/only/_CoqProject +++ b/test-suite/coq-makefile/only/_CoqProject @@ -3,7 +3,7 @@ -I src/ ./src/test_plugin.mlpack -./src/test.ml4 +./src/test.mlg ./src/test.mli ./src/test_aux.ml ./src/test_aux.mli diff --git a/test-suite/coq-makefile/plugin1/_CoqProject b/test-suite/coq-makefile/plugin1/_CoqProject index 4eddc9d708..ab7876d868 100644 --- a/test-suite/coq-makefile/plugin1/_CoqProject +++ b/test-suite/coq-makefile/plugin1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mllib -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/plugin2/_CoqProject b/test-suite/coq-makefile/plugin2/_CoqProject index 0bf1e07f25..94eed53130 100644 --- a/test-suite/coq-makefile/plugin2/_CoqProject +++ b/test-suite/coq-makefile/plugin2/_CoqProject @@ -3,7 +3,7 @@ -I src/ src/test_plugin.mllib -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/plugin3/_CoqProject b/test-suite/coq-makefile/plugin3/_CoqProject index 2028d49a8b..8e8a7ab074 100644 --- a/test-suite/coq-makefile/plugin3/_CoqProject +++ b/test-suite/coq-makefile/plugin3/_CoqProject @@ -3,7 +3,7 @@ -I src/ ./src/test_plugin.mllib -./src/test.ml4 +./src/test.mlg ./src/test.mli ./src/test_aux.ml ./src/test_aux.mli diff --git a/test-suite/coq-makefile/quick2vo/_CoqProject b/test-suite/coq-makefile/quick2vo/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/quick2vo/_CoqProject +++ b/test-suite/coq-makefile/quick2vo/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/template/init.sh b/test-suite/coq-makefile/template/init.sh index 2e066d30d9..30be5e6456 100755 --- a/test-suite/coq-makefile/template/init.sh +++ b/test-suite/coq-makefile/template/init.sh @@ -11,7 +11,7 @@ mkdir -p theories/sub cp ../../template/theories/sub/testsub.v theories/sub cp ../../template/theories/test.v theories -cp ../../template/src/test.ml4 src +cp ../../template/src/test.mlg src cp ../../template/src/test_aux.mli src cp ../../template/src/test.mli src cp ../../template/src/test_plugin.mlpack src diff --git a/test-suite/coq-makefile/template/src/test.ml4 b/test-suite/coq-makefile/template/src/test.mlg index 72765abe04..7a166f3b98 100644 --- a/test-suite/coq-makefile/template/src/test.ml4 +++ b/test-suite/coq-makefile/template/src/test.mlg @@ -1,13 +1,17 @@ +{ open Ltac_plugin +} DECLARE PLUGIN "test_plugin" +{ let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";; +} VERNAC COMMAND EXTEND Test CLASSIFIED AS SIDEFF - | [ "TestCommand" ] -> [ () ] + | [ "TestCommand" ] -> { () } END TACTIC EXTEND test -| [ "test_tactic" ] -> [ Test_aux.tac ] +| [ "test_tactic" ] -> { Test_aux.tac } END diff --git a/test-suite/coq-makefile/uninstall1/_CoqProject b/test-suite/coq-makefile/uninstall1/_CoqProject index 35792066bb..aa9473eaf0 100644 --- a/test-suite/coq-makefile/uninstall1/_CoqProject +++ b/test-suite/coq-makefile/uninstall1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/uninstall2/_CoqProject b/test-suite/coq-makefile/uninstall2/_CoqProject index d2a547d47b..0068554d72 100644 --- a/test-suite/coq-makefile/uninstall2/_CoqProject +++ b/test-suite/coq-makefile/uninstall2/_CoqProject @@ -3,7 +3,7 @@ -I src/ src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/validate1/_CoqProject b/test-suite/coq-makefile/validate1/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/validate1/_CoqProject +++ b/test-suite/coq-makefile/validate1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/vio2vo/_CoqProject b/test-suite/coq-makefile/vio2vo/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/vio2vo/_CoqProject +++ b/test-suite/coq-makefile/vio2vo/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/misc/poly-capture-global-univs/_CoqProject b/test-suite/misc/poly-capture-global-univs/_CoqProject index 70ec246062..e5dc3cff56 100644 --- a/test-suite/misc/poly-capture-global-univs/_CoqProject +++ b/test-suite/misc/poly-capture-global-univs/_CoqProject @@ -1,7 +1,7 @@ -Q theories Evil -I src -src/evil.ml4 +src/evil.mlg src/evilImpl.ml src/evilImpl.mli src/evil_plugin.mlpack diff --git a/test-suite/misc/poly-capture-global-univs/src/evil.ml4 b/test-suite/misc/poly-capture-global-univs/src/evil.ml4 deleted file mode 100644 index 565e979aaa..0000000000 --- a/test-suite/misc/poly-capture-global-univs/src/evil.ml4 +++ /dev/null @@ -1,9 +0,0 @@ - -open Stdarg -open EvilImpl - -DECLARE PLUGIN "evil_plugin" - -VERNAC COMMAND FUNCTIONAL EXTEND VernacEvil CLASSIFIED AS SIDEFF -| [ "Evil" ident(x) ident(y) ] -> [ fun ~atts ~st -> evil x y; st ] -END diff --git a/test-suite/misc/poly-capture-global-univs/src/evil.mlg b/test-suite/misc/poly-capture-global-univs/src/evil.mlg new file mode 100644 index 0000000000..edd22b1d29 --- /dev/null +++ b/test-suite/misc/poly-capture-global-univs/src/evil.mlg @@ -0,0 +1,10 @@ +{ +open Stdarg +open EvilImpl +} + +DECLARE PLUGIN "evil_plugin" + +VERNAC COMMAND EXTEND VernacEvil CLASSIFIED AS SIDEFF +| [ "Evil" ident(x) ident(y) ] -> { evil x y } +END diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index cef7d1a702..46784d1897 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -1,5 +1,7 @@ [< 0 > + < 1 > * < 2 >] : nat +[< b > + < b > * < 2 >] + : nat [<< # 0 >>] : option nat [1 {f 1}] diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 9738ce5a5e..6bdbf1bed5 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -10,6 +10,10 @@ Notation "x * y" := (Nat.mul x y) (in custom myconstr at level 4). Notation "< x >" := x (in custom myconstr at level 3, x constr at level 10). Check [ < 0 > + < 1 > * < 2 >]. +Axiom a : nat. +Notation b := a. +Check [ < b > + < a > * < 2 >]. + Declare Custom Entry anotherconstr. Notation "[ x ]" := x (x custom myconstr at level 6). diff --git a/test-suite/output/RecordFieldErrors.out b/test-suite/output/RecordFieldErrors.out new file mode 100644 index 0000000000..5b67f632c9 --- /dev/null +++ b/test-suite/output/RecordFieldErrors.out @@ -0,0 +1,14 @@ +The command has indeed failed with message: +unit: Not a projection. +The command has indeed failed with message: +unit: Not a projection. +The command has indeed failed with message: +This record contains fields of both t and t'. +The command has indeed failed with message: +unit: Not a projection. +The command has indeed failed with message: +This record defines several times the field foo. +The command has indeed failed with message: +This record defines several times the field unit. +The command has indeed failed with message: +unit: Not a projection of inductive t. diff --git a/test-suite/output/RecordFieldErrors.v b/test-suite/output/RecordFieldErrors.v new file mode 100644 index 0000000000..27aa07822b --- /dev/null +++ b/test-suite/output/RecordFieldErrors.v @@ -0,0 +1,38 @@ +(** Check that various errors in record fields are reported with the correct +underlying issue. *) + +Record t := + { foo: unit }. + +Record t' := + { bar: unit }. + +Fail Check {| unit := tt |}. +(* unit: Not a projection. *) + +Fail Check {| unit := tt; + foo := tt |}. +(* unit: Not a projection. *) + +Fail Check {| foo := tt; + bar := tt |}. +(* This record contains fields of both t and t'. *) + +Fail Check {| unit := tt; + unit := tt |}. +(* unit: Not a projection. *) + +Fail Check {| foo := tt; + foo := tt |}. +(* This record defines several times the field foo. *) + +Fail Check {| foo := tt; + unit := tt; + unit := tt |}. +(* This is slightly wrong (would prefer "unit: Not a projection."), but it's +acceptable and seems an unlikely mistake. *) +(* This record defines several times the field unit. *) + +Fail Check {| foo := tt; + unit := tt |}. +(* unit: Not a projection of inductive t. *) |