diff options
Diffstat (limited to 'test-suite')
61 files changed, 1483 insertions, 123 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 1d21b4b5e0..265c2eafa7 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -643,7 +643,7 @@ vio: $(patsubst %.v,%.vio.log,$(wildcard vio/*.v)) %.vio.log:%.v @echo "TEST $<" $(HIDE){ \ - $(coqc) -quick -R vio vio $* 2>&1 && \ + $(coqc) -vio -R vio vio $* 2>&1 && \ $(coqc) -R vio vio -vio2vo $*.vio 2>&1 && \ $(coqchk) -R vio vio -norec $(subst /,.,$*) 2>&1; \ if [ $$? = 0 ]; then \ diff --git a/test-suite/README.md b/test-suite/README.md index a2d5905710..96926f70b9 100644 --- a/test-suite/README.md +++ b/test-suite/README.md @@ -67,7 +67,7 @@ See [`test-suite/Makefile`](Makefile) for more information. ## Adding a test Regression tests for closed bugs should be added to -[`bugs/closed`](bugs/closed), as `1234.v` where `1234` is the bug number. +[`bugs/closed`](bugs/closed), as `bug_1234.v` where `1234` is the bug number. Files in this directory are tested for successful compilation. When you fix a bug, you should usually add a regression test here as well. diff --git a/test-suite/bugs/bug_11140.v b/test-suite/bugs/bug_11140.v new file mode 100644 index 0000000000..ca806ea324 --- /dev/null +++ b/test-suite/bugs/bug_11140.v @@ -0,0 +1,11 @@ +Axiom T : nat -> Prop. +Axiom f : forall x, T x. +Arguments f & x. + +Lemma test : (f (1 + _) : T 2) = f 2. +match goal with +| |- (f (1 + 1) = f 2) => idtac +| |- (f 2 = f 2) => fail (* Issue 11140 *) +| |- _ => fail +end. +Abort. diff --git a/test-suite/bugs/closed/bug_11133.v b/test-suite/bugs/closed/bug_11133.v new file mode 100644 index 0000000000..87f15a4a19 --- /dev/null +++ b/test-suite/bugs/closed/bug_11133.v @@ -0,0 +1,18 @@ +Module Type Universe. +Parameter U : nat. +End Universe. + +Module Univ_prop (Univ : Universe). +Include Univ. +End Univ_prop. + +Module Monad (Univ : Universe). +Module UP := (Univ_prop Univ). +End Monad. + +Module Rules (Univ:Universe). +Module MP := Monad Univ. +Include MP. +Import UP. +Definition M := UP.U. (* anomaly here *) +End Rules. diff --git a/test-suite/bugs/closed/bug_11168.v b/test-suite/bugs/closed/bug_11168.v new file mode 100644 index 0000000000..6e109e33e6 --- /dev/null +++ b/test-suite/bugs/closed/bug_11168.v @@ -0,0 +1,5 @@ +Axiom f : forall T, T. +Arguments f &. +Check f _ _. +Check f (_ -> _) _. +Check f (forall x, _) _. diff --git a/test-suite/bugs/closed/bug_11360.v b/test-suite/bugs/closed/bug_11360.v new file mode 100644 index 0000000000..d8bc4a9f02 --- /dev/null +++ b/test-suite/bugs/closed/bug_11360.v @@ -0,0 +1,6 @@ +Section S. + Variable (A:Type). + #[universes(template)] + Inductive bar (d:A) := . +End S. +Check bar nat 0. diff --git a/test-suite/bugs/closed/bug_11421.v b/test-suite/bugs/closed/bug_11421.v new file mode 100644 index 0000000000..8ddf05c888 --- /dev/null +++ b/test-suite/bugs/closed/bug_11421.v @@ -0,0 +1 @@ +Fail Definition plus1_plus1 : Type@{Set+1} := Type@{Set+1}. diff --git a/test-suite/bugs/closed/bug_11515.v b/test-suite/bugs/closed/bug_11515.v new file mode 100644 index 0000000000..fe4ba87447 --- /dev/null +++ b/test-suite/bugs/closed/bug_11515.v @@ -0,0 +1,7 @@ +Require Import Ltac2.Ltac2. + +Lemma foo : + True. +Proof. + Fail rewrite _. +Abort. diff --git a/test-suite/bugs/closed/bug_11553.v b/test-suite/bugs/closed/bug_11553.v new file mode 100644 index 0000000000..a4a4353cd6 --- /dev/null +++ b/test-suite/bugs/closed/bug_11553.v @@ -0,0 +1,34 @@ +Definition var := nat. +Module Import A. +Class Rename (term : Type) := rename : (var -> var) -> term -> term. +End A. + +Inductive tm : Type := + (* | tv : vl_ -> tm *) + with vl_ : Type := + | var_vl : var -> vl_. + +Definition vl := vl_. + +Fixpoint tm_rename (sb : var -> var) (t : tm) : tm := + let b := vl_rename : Rename vl in + match t with + end +with +vl_rename (sb : var -> var) v : vl := + let a := tm_rename : Rename tm in + let b := vl_rename : Rename vl in + match v with + | var_vl x => var_vl (sb x) + end. + +Instance rename_vl : Rename vl := vl_rename. + +Lemma foo ξ x: rename_vl ξ (var_vl x) = var_vl x. +(* Succeeds *) +cbn. Abort. + +Lemma foo ξ x: rename ξ (var_vl x) = var_vl x. +(* Fails *) +cbn. +Abort. diff --git a/test-suite/bugs/closed/bug_2729.v b/test-suite/bugs/closed/bug_2729.v index ff08bdc6bb..52cc34beb3 100644 --- a/test-suite/bugs/closed/bug_2729.v +++ b/test-suite/bugs/closed/bug_2729.v @@ -82,7 +82,7 @@ Inductive SequenceBase (pu : PatchUniverse) (p : pu_type from mid) (qs : SequenceBase pu mid to), SequenceBase pu from to. -Arguments Nil [pu cxt]. +Arguments Nil {pu cxt}. Arguments Cons [pu from mid to]. Program Fixpoint insertBase {pu : PatchUniverse} diff --git a/test-suite/bugs/closed/bug_5617.v b/test-suite/bugs/closed/bug_5617.v new file mode 100644 index 0000000000..c18e79295c --- /dev/null +++ b/test-suite/bugs/closed/bug_5617.v @@ -0,0 +1,8 @@ +Set Primitive Projections. +Record T X := { F : X }. + +Fixpoint f (n : nat) : nat := +match n with +| 0 => 0 +| S m => F _ {| F := f |} m +end. diff --git a/test-suite/complexity/injection.v b/test-suite/complexity/injection.v index 298a07c1c4..7022987096 100644 --- a/test-suite/complexity/injection.v +++ b/test-suite/complexity/injection.v @@ -47,7 +47,7 @@ Parameter mkJoinmap : forall (key: Type) (t: Type) (j: joinable t), joinmap key j. Parameter ADMIT: forall p: Prop, p. -Arguments ADMIT [p]. +Arguments ADMIT {p}. Module Share. Parameter jb : joinable bool. diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/run.sh index e1f17725dc..13e484b852 100755 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/run.sh +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/run.sh @@ -5,20 +5,14 @@ set -e cd "$(dirname "${BASH_SOURCE[0]}")" -python2 "$COQLIB"/tools/make-one-time-file.py time-of-build.log.in time-of-build-pretty.log2 || exit $? -python3 "$COQLIB"/tools/make-one-time-file.py time-of-build.log.in time-of-build-pretty.log3 || exit $? +"$COQLIB"/tools/make-one-time-file.py time-of-build.log.in time-of-build-pretty.log || exit $? -diff -u time-of-build-pretty.log.expected time-of-build-pretty.log2 || exit $? -diff -u time-of-build-pretty.log.expected time-of-build-pretty.log3 || exit $? +diff -u time-of-build-pretty.log.expected time-of-build-pretty.log || exit $? -cat time-of-build.log.in | python2 "$COQLIB"/tools/make-one-time-file.py - time-of-build-pretty.log2 || exit $? -cat time-of-build.log.in | python3 "$COQLIB"/tools/make-one-time-file.py - time-of-build-pretty.log3 || exit $? +cat time-of-build.log.in | "$COQLIB"/tools/make-one-time-file.py - time-of-build-pretty.log || exit $? -diff -u time-of-build-pretty.log.expected time-of-build-pretty.log2 || exit $? -diff -u time-of-build-pretty.log.expected time-of-build-pretty.log3 || exit $? +diff -u time-of-build-pretty.log.expected time-of-build-pretty.log || exit $? -(python2 "$COQLIB"/tools/make-one-time-file.py time-of-build.log.in - || exit $?) > time-of-build-pretty.log2 -(python3 "$COQLIB"/tools/make-one-time-file.py time-of-build.log.in - || exit $?) > time-of-build-pretty.log3 +("$COQLIB"/tools/make-one-time-file.py time-of-build.log.in - || exit $?) > time-of-build-pretty.log -diff -u time-of-build-pretty.log.expected time-of-build-pretty.log2 || exit $? -diff -u time-of-build-pretty.log.expected time-of-build-pretty.log3 || exit $? +diff -u time-of-build-pretty.log.expected time-of-build-pretty.log || exit $? diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh index 9f3b648aa3..cfacf738a3 100755 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh @@ -9,3 +9,4 @@ export COQLIB ./001-correct-diff-sorting-order/run.sh ./002-single-file-sorting/run.sh +./003-non-utf8/run.sh diff --git a/test-suite/coqdoc/bug11353.html.out b/test-suite/coqdoc/bug11353.html.out new file mode 100644 index 0000000000..0b4b4b6e37 --- /dev/null +++ b/test-suite/coqdoc/bug11353.html.out @@ -0,0 +1,39 @@ +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" +"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> +<html xmlns="http://www.w3.org/1999/xhtml"> +<head> +<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> +<link href="coqdoc.css" rel="stylesheet" type="text/css" /> +<title>Coqdoc.bug11353</title> +</head> + +<body> + +<div id="page"> + +<div id="header"> +</div> + +<div id="main"> + +<h1 class="libtitle">Library Coqdoc.bug11353</h1> + +<div class="code"> +<span class="id" title="keyword">Definition</span> <a name="a"><span class="id" title="definition">a</span></a> := 0. #[ <span class="id" title="var">universes</span>( <span class="id" title="var">template</span>) ]<br/> +<span class="id" title="keyword">Inductive</span> <a name="mysum"><span class="id" title="inductive">mysum</span></a> (<span class="id" title="var">A</span> <span class="id" title="var">B</span>:<span class="id" title="keyword">Type</span>) : <span class="id" title="keyword">Type</span> :=<br/> + | <a name="myinl"><span class="id" title="constructor">myinl</span></a> : <a class="idref" href="Coqdoc.bug11353.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="Coqdoc.bug11353.html#mysum"><span class="id" title="inductive">mysum</span></a> <a class="idref" href="Coqdoc.bug11353.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="Coqdoc.bug11353.html#B"><span class="id" title="variable">B</span></a><br/> + | <a name="myinr"><span class="id" title="constructor">myinr</span></a> : <a class="idref" href="Coqdoc.bug11353.html#B"><span class="id" title="variable">B</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="Coqdoc.bug11353.html#mysum"><span class="id" title="inductive">mysum</span></a> <a class="idref" href="Coqdoc.bug11353.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="Coqdoc.bug11353.html#B"><span class="id" title="variable">B</span></a>.<br/> + +<br/> +#[<span class="id" title="var">local</span>]<span class="id" title="keyword">Definition</span> <a name="b"><span class="id" title="definition">b</span></a> := 1.<br/> +</div> +</div> + +<div id="footer"> +<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a> +</div> + +</div> + +</body> +</html>
\ No newline at end of file diff --git a/test-suite/coqdoc/bug11353.tex.out b/test-suite/coqdoc/bug11353.tex.out new file mode 100644 index 0000000000..a6478682d8 --- /dev/null +++ b/test-suite/coqdoc/bug11353.tex.out @@ -0,0 +1,34 @@ +\documentclass[12pt]{report} +\usepackage[utf8x]{inputenc} + +%Warning: tipa declares many non-standard macros used by utf8x to +%interpret utf8 characters but extra packages might have to be added +%such as "textgreek" for Greek letters not already in tipa +%or "stmaryrd" for mathematical symbols. +%Utf8 codes missing a LaTeX interpretation can be defined by using +%\DeclareUnicodeCharacter{code}{interpretation}. +%Use coqdoc's option -p to add new packages or declarations. +\usepackage{tipa} + +\usepackage[T1]{fontenc} +\usepackage{fullpage} +\usepackage{coqdoc} +\usepackage{amsmath,amssymb} +\usepackage{url} +\begin{document} +\coqlibrary{Coqdoc.bug11353}{Library }{Coqdoc.bug11353} + +\begin{coqdoccode} +\coqdocnoindent +\coqdockw{Definition} \coqdef{Coqdoc.bug11353.a}{a}{\coqdocdefinition{a}} := 0. \#[ \coqdocvar{universes}( \coqdocvar{template}) ]\coqdoceol +\coqdocnoindent +\coqdockw{Inductive} \coqdef{Coqdoc.bug11353.mysum}{mysum}{\coqdocinductive{mysum}} (\coqdocvar{A} \coqdocvar{B}:\coqdockw{Type}) : \coqdockw{Type} :=\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqdef{Coqdoc.bug11353.myinl}{myinl}{\coqdocconstructor{myinl}} : \coqdocvariable{A} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqref{Coqdoc.bug11353.mysum}{\coqdocinductive{mysum}} \coqdocvariable{A} \coqdocvariable{B}\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqdef{Coqdoc.bug11353.myinr}{myinr}{\coqdocconstructor{myinr}} : \coqdocvariable{B} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqref{Coqdoc.bug11353.mysum}{\coqdocinductive{mysum}} \coqdocvariable{A} \coqdocvariable{B}.\coqdoceol +\coqdocemptyline +\coqdocnoindent +\#[\coqdocvar{local}]\coqdockw{Definition} \coqdef{Coqdoc.bug11353.b}{b}{\coqdocdefinition{b}} := 1.\coqdoceol +\end{coqdoccode} +\end{document} diff --git a/test-suite/coqdoc/bug11353.v b/test-suite/coqdoc/bug11353.v new file mode 100644 index 0000000000..b68902c8cc --- /dev/null +++ b/test-suite/coqdoc/bug11353.v @@ -0,0 +1,7 @@ +(* -*- coq-prog-args: ("-g") -*- *) +Definition a := 0. #[ (* templatize *) universes( template) ] +Inductive mysum (A B:Type) : Type := + | myinl : A -> mysum A B + | myinr : B -> mysum A B. + +#[local]Definition b := 1. diff --git a/test-suite/failure/Template.v b/test-suite/failure/Template.v deleted file mode 100644 index 75b2a56169..0000000000 --- a/test-suite/failure/Template.v +++ /dev/null @@ -1,32 +0,0 @@ -(* -Module TestUnsetTemplateCheck. - Unset Template Check. - - Section Foo. - - Context (A : Type). - - Definition cstr := nat : ltac:(let ty := type of A in exact ty). - - Inductive myind := - | cons : A -> myind. - End Foo. - - (* Can only succeed if no template check is performed *) - Check myind True : Prop. - - Print Assumptions myind. - (* - Axioms: - myind is template polymorphic on all its universe parameters. - *) - About myind. -(* -myind : Type@{Top.60} -> Type@{Top.60} - -myind is assumed template universe polymorphic on Top.60 -Argument scope is [type_scope] -Expands to: Inductive Top.TestUnsetTemplateCheck.myind -*) -End TestUnsetTemplateCheck. -*) diff --git a/test-suite/ltac2/array_lib.v b/test-suite/ltac2/array_lib.v new file mode 100644 index 0000000000..31227eaddb --- /dev/null +++ b/test-suite/ltac2/array_lib.v @@ -0,0 +1,181 @@ +Require Import Ltac2.Ltac2. +Import Ltac2.Message. +Import Ltac2.Array. +Require Ltac2.List. +Require Ltac2.Int. + +(* Array/List comparison functions which throw an exception on unequal *) + +Ltac2 Type exn ::= [ Regression_Test_Failure ]. + +Ltac2 check_eq_int a l := + List.iter2 + (fun a b => match Int.equal a b with true => () | false => Control.throw Regression_Test_Failure end) + (to_list a) l. + +Ltac2 check_eq_bool a l := + List.iter2 + (fun a b => match Bool.eq a b with true => () | false => Control.throw Regression_Test_Failure end) + (to_list a) l. + +Ltac2 check_eq_int_matrix m ll := + List.iter2 (fun a b => check_eq_int a b) (to_list m) ll. + +Ltac2 check_eq_bool_matrix m ll := + List.iter2 (fun a b => check_eq_bool a b) (to_list m) ll. + +(* The below printing functions are mostly for debugging below test cases *) + +Ltac2 print2 m1 m2 := print (Message.concat m1 m2). +Ltac2 print3 m1 m2 m3 := print2 m1 (Message.concat m2 m3). + +Ltac2 print_int_array a := + iteri (fun i x => print3 (of_int i) (of_string "=") (of_int x)) a. + +Ltac2 of_bool b := match b with true=>of_string "true" | false=>of_string "false" end. + +Ltac2 print_bool_array a := + iteri (fun i x => print3 (of_int i) (of_string "=") (of_bool x)) a. + +Ltac2 print_int_list a := + List.iteri (fun i x => print3 (of_int i) (of_string "=") (of_int x)) a. + +Goal True. + (* Test failure *) + Fail check_eq_int ((init 3 (fun i => (Int.add i 10)))) [10;11;13]. + + (* test empty with int *) + check_eq_int (empty ()) []. + check_eq_int (append (empty ()) (init 3 (fun i => (Int.add i 10)))) [10;11;12]. + check_eq_int (append (init 3 (fun i => (Int.add i 10))) (empty ())) [10;11;12]. + + (* test empty with bool *) + check_eq_bool (empty ()) []. + check_eq_bool (append (empty ()) (init 3 (fun i => (Int.ge i 2)))) [false;false;true]. + check_eq_bool (append (init 3 (fun i => (Int.ge i 2))) (empty ())) [false;false;true]. + + (* test init with int *) + check_eq_int (init 0 (fun i => (Int.add i 10))) []. + check_eq_int (init 4 (fun i => (Int.add i 10))) [10;11;12;13]. + + (* test init with bool *) + check_eq_bool (init 0 (fun i => (Int.ge i 2))) []. + check_eq_bool (init 4 (fun i => (Int.ge i 2))) [false;false;true;true]. + + (* test make_matrix, set, get *) + let a := make_matrix 4 3 1 in + Array.set (Array.get a 1) 2 0; + check_eq_int_matrix a [[1;1;1];[1;1;0];[1;1;1];[1;1;1]]. + + let a := make_matrix 3 4 false in + Array.set (Array.get a 2) 1 true; + check_eq_bool_matrix a [[false;false;false;false];[false;false;false;false];[false;true;false;false]]. + + (* test copy *) + let a := init 4 (fun i => (Int.add i 10)) in + let b := copy a in + check_eq_int b [10;11;12;13]. + + (* test append *) + let a := init 3 (fun i => (Int.add i 10)) in + let b := init 4 (fun i => (Int.add i 20)) in + check_eq_int (append a b) [10;11;12;20;21;22;23]. + + (* test concat *) + let a := init 3 (fun i => (Int.add i 10)) in + let b := init 4 (fun i => (Int.add i 20)) in + let c := init 5 (fun i => (Int.add i 30)) in + check_eq_int (concat (a::b::c::[])) [10;11;12;20;21;22;23;30;31;32;33;34]. + + (* test sub *) + let a := init 10 (fun i => (Int.add i 10)) in + let b := (sub a 3 0) in + let c := (append b (init 3 (fun i => (Int.add i 10)))) in + check_eq_int b []; + check_eq_int c [10;11;12]. + + let a := init 10 (fun i => (Int.add i 10)) in + let b := (sub a 3 4) in + check_eq_int b [13;14;15;16]. + + (* test fill *) + let a := init 10 (fun i => (Int.add i 10)) in + fill a 3 4 0; + check_eq_int a [10;11;12;0;0;0;0;17;18;19]. + + (* test blit *) + let a := init 10 (fun i => (Int.add i 10)) in + let b := init 10 (fun i => (Int.add i 20)) in + blit a 5 b 3 4; + check_eq_int b [20;21;22;15;16;17;18;27;28;29]. + + (* test iter *) + let a := init 4 (fun i => (Int.add i 3)) in + let b := init 10 (fun i => 10) in + iter (fun x => Array.set b x x) a; + check_eq_int b [10;10;10;3;4;5;6;10;10;10]. + + (* test iter2 *) + let a := init 4 (fun i => (Int.add i 2)) in + let b := init 4 (fun i => (Int.add i 4)) in + let c := init 8 (fun i => 10) in + iter2 (fun x y => Array.set c x y) a b; + check_eq_int c [10;10;4;5;6;7;10;10]. + + (* test map *) + let a := init 4 (fun i => (Int.add i 10)) in + check_eq_bool (map (fun i => (Int.ge i 12)) a) [false;false;true;true]. + + (* test map2 *) + let a := init 4 (fun i => (Int.add 10 i)) in + let b := init 4 (fun i => (Int.sub 13 i)) in + check_eq_bool (map2 (fun x y => (Int.ge x y)) a b) [false;false;true;true]. + + (* test iteri *) + let a := init 4 (fun i => (Int.add i 10)) in + let m := make_matrix 4 2 100 in + iteri (fun i x => Array.set (Array.get m i) 0 i; Array.set (Array.get m i) 1 x) a; + check_eq_int_matrix m [[0;10];[1;11];[2;12];[3;13]]. + + (* test mapi *) + let a := init 4 (fun i => (Int.sub 3 i)) in + check_eq_bool (mapi (fun i x => (Int.ge i x)) a) [false;false;true;true]. + + (* to_list is already tested in check_eq_... *) + + (* test of_list *) + check_eq_int (of_list ([0;1;2;3])) [0;1;2;3]. + + (* test fold_left *) + let a := init 4 (fun i => (Int.add 10 i)) in + check_eq_int (of_list (fold_left (fun a b => b::a) [] a)) [13;12;11;10]. + + (* test fold_right *) + let a := init 4 (fun i => (Int.add 10 i)) in + check_eq_int (of_list (fold_right (fun a b => b::a) [] a)) [10;11;12;13]. + + (* test exist *) + let a := init 4 (fun i => (Int.add 10 i)) in + let l := [ + exist (fun x => Int.equal x 10) a; + exist (fun x => Int.equal x 13) a; + exist (fun x => Int.equal x 14) a] in + check_eq_bool (of_list l) [true;true;false]. + + (* test for_all *) + let a := init 4 (fun i => (Int.add 10 i)) in + let l := [ + for_all (fun x => Int.lt x 14) a; + for_all (fun x => Int.lt x 13) a] in + check_eq_bool (of_list l) [true;false]. + + (* test mem *) + let a := init 4 (fun i => (Int.add 10 i)) in + let l := [ + mem Int.equal 10 a; + mem Int.equal 13 a; + mem Int.equal 14 a] in + check_eq_bool (of_list l) [true;true;false]. + +exact I. +Qed. diff --git a/test-suite/micromega/bug_11191a.v b/test-suite/micromega/bug_11191a.v new file mode 100644 index 0000000000..57c1d7d52f --- /dev/null +++ b/test-suite/micromega/bug_11191a.v @@ -0,0 +1,6 @@ +Require Import ZArith Lia. + +Goal forall p n, (0 < Z.pos (p ^ n))%Z. + intros. + lia. +Qed. diff --git a/test-suite/micromega/bug_11191b.v b/test-suite/micromega/bug_11191b.v new file mode 100644 index 0000000000..007470c5b3 --- /dev/null +++ b/test-suite/micromega/bug_11191b.v @@ -0,0 +1,6 @@ +Require Import ZArith Lia. + +Goal forall p, (0 < Z.pos (p ^ 2))%Z. + intros. + lia. +Qed. diff --git a/test-suite/micromega/bug_11436.v b/test-suite/micromega/bug_11436.v new file mode 100644 index 0000000000..fc6ccbb233 --- /dev/null +++ b/test-suite/micromega/bug_11436.v @@ -0,0 +1,19 @@ +Require Import ZArith Lia. +Local Open Scope Z_scope. + +Unset Lia Cache. + +Goal forall a q q0 q1 r r0 r1: Z, + 0 <= a < 2 ^ 64 -> + r1 = 4 * q + r -> + 0 <= r < 4 -> + a = 4 * q0 + r0 -> + 0 <= r0 < 4 -> + a + 4 = 2 ^ 64 * q1 + r1 -> + 0 <= r1 < 2 ^ 64 -> + r = r0. +Proof. + intros. + (* subst. *) + Time lia. +Qed. diff --git a/test-suite/micromega/evars_loops_in_8_10_fixed_8_11.v b/test-suite/micromega/evars_loops_in_8_10_fixed_8_11.v new file mode 100644 index 0000000000..a53c160e45 --- /dev/null +++ b/test-suite/micromega/evars_loops_in_8_10_fixed_8_11.v @@ -0,0 +1,4 @@ +Require Import Lia. +Goal forall n (B: n >= 0), exists Goal1 Goal2 Goal3, + (0 * (Goal1 * Goal2 + Goal1) <> Goal3 * 0 * (Goal1 * S Goal2)). +Proof. eexists _, _, _. Fail lia. Abort. diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v index 9efb81a901..36b4243ef8 100644 --- a/test-suite/micromega/square.v +++ b/test-suite/micromega/square.v @@ -11,15 +11,14 @@ Open Scope Z_scope. Lemma Zabs_square : forall x, (Z.abs x)^2 = x^2. Proof. - intros ; case (Zabs_dec x) ; intros ; nia. + intros ; nia. Qed. -Hint Resolve Z.abs_nonneg Zabs_square. Lemma integer_statement : ~exists n, exists p, n^2 = 2*p^2 /\ n <> 0. Proof. intros [n [p [Heq Hnz]]]; pose (n' := Z.abs n); pose (p':=Z.abs p). assert (facts : 0 <= Z.abs n /\ 0 <= Z.abs p /\ Z.abs n^2=n^2 - /\ Z.abs p^2 = p^2) by auto. + /\ Z.abs p^2 = p^2) by auto using Z.abs_nonneg, Zabs_square. assert (H : (0 < n' /\ 0 <= p' /\ n' ^2 = 2* p' ^2)) by (destruct facts as [Hf1 [Hf2 [Hf3 Hf4]]]; unfold n', p' ; nia). generalize p' H; elim n' using (well_founded_ind (Zwf_well_founded 0)); clear. @@ -45,10 +44,7 @@ Proof. intros. destruct x. simpl. - unfold Z.pow_pos. - simpl. - rewrite Pos.mul_1_r. - reflexivity. + lia. Qed. Theorem sqrt2_not_rational : ~exists x:Q, x^2==2#1. diff --git a/test-suite/misc/quick-include.sh b/test-suite/misc/quick-include.sh index 96bdee2fc2..e60fb48bca 100755 --- a/test-suite/misc/quick-include.sh +++ b/test-suite/misc/quick-include.sh @@ -1,5 +1,5 @@ #!/bin/sh set -e -$coqc -R misc/quick-include/ QuickInclude -quick misc/quick-include/file1.v -$coqc -R misc/quick-include/ QuickInclude -quick misc/quick-include/file2.v +$coqc -R misc/quick-include/ QuickInclude -vio misc/quick-include/file1.v +$coqc -R misc/quick-include/ QuickInclude -vio misc/quick-include/file2.v diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 5093e785de..26ebd8efc3 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -86,8 +86,8 @@ Sequences of implicit arguments must be of different lengths. The command has indeed failed with message: Some argument names are duplicated: F The command has indeed failed with message: -Argument number 2 (anonymous in original definition) cannot be declared -implicit. +Argument number 3 is a trailing implicit, so it can't be declared non +maximal. Please use { } instead of [ ]. The command has indeed failed with message: Extra arguments: y. The command has indeed failed with message: diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v index 9713a9dbbe..6ac09cf771 100644 --- a/test-suite/output/Arguments_renaming.v +++ b/test-suite/output/Arguments_renaming.v @@ -49,7 +49,6 @@ Check @myplus. Fail Arguments eq_refl {F g}, [H] k. Fail Arguments eq_refl {F}, [F] : rename. Fail Arguments eq_refl {F F}, [F] F : rename. -Fail Arguments eq {F} x [z] : rename. +Fail Arguments eq {A} x [z] : rename. Fail Arguments eq {F} x z y. Fail Arguments eq {R} s t. - diff --git a/test-suite/output/ErrorInModule.v b/test-suite/output/ErrorInModule.v index b2e3c3e923..fbb3c6bdab 100644 --- a/test-suite/output/ErrorInModule.v +++ b/test-suite/output/ErrorInModule.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-quick") -*- *) +(* -*- mode: coq; coq-prog-args: ("-vio") -*- *) Module M. Definition foo := nonexistent. End M. diff --git a/test-suite/output/ErrorInSection.v b/test-suite/output/ErrorInSection.v index 505c5ce378..a961330b81 100644 --- a/test-suite/output/ErrorInSection.v +++ b/test-suite/output/ErrorInSection.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-quick") -*- *) +(* -*- mode: coq; coq-prog-args: ("-vio") -*- *) Section S. Definition foo := nonexistent. End S. diff --git a/test-suite/output/ExtractionString.out b/test-suite/output/ExtractionString.out new file mode 100644 index 0000000000..2a101d9cea --- /dev/null +++ b/test-suite/output/ExtractionString.out @@ -0,0 +1,52 @@ +(** val str : string **) + +let str = + String ((Ascii (False, False, True, False, True, False, True, False)), + (String ((Ascii (False, False, False, True, False, True, True, False)), + (String ((Ascii (True, False, False, True, False, True, True, False)), + (String ((Ascii (True, True, False, False, True, True, True, False)), + (String ((Ascii (False, False, False, False, False, True, False, False)), + (String ((Ascii (True, False, False, True, False, True, True, False)), + (String ((Ascii (True, True, False, False, True, True, True, False)), + (String ((Ascii (False, False, False, False, False, True, False, False)), + (String ((Ascii (True, False, False, False, False, True, True, False)), + (String ((Ascii (False, False, False, False, False, True, False, False)), + (String ((Ascii (True, True, False, False, True, True, True, False)), + (String ((Ascii (False, False, True, False, True, True, True, False)), + (String ((Ascii (False, True, False, False, True, True, True, False)), + (String ((Ascii (True, False, False, True, False, True, True, False)), + (String ((Ascii (False, True, True, True, False, True, True, False)), + (String ((Ascii (True, True, True, False, False, True, True, False)), + EmptyString))))))))))))))))))))))))))))))) +str :: String +str = + String0 (Ascii False False True False True False True False) (String0 + (Ascii False False False True False True True False) (String0 (Ascii True + False False True False True True False) (String0 (Ascii True True False + False True True True False) (String0 (Ascii False False False False False + True False False) (String0 (Ascii True False False True False True True + False) (String0 (Ascii True True False False True True True False) + (String0 (Ascii False False False False False True False False) (String0 + (Ascii True False False False False True True False) (String0 (Ascii + False False False False False True False False) (String0 (Ascii True True + False False True True True False) (String0 (Ascii False False True False + True True True False) (String0 (Ascii False True False False True True + True False) (String0 (Ascii True False False True False True True False) + (String0 (Ascii False True True True False True True False) (String0 + (Ascii True True True False False True True False) + EmptyString))))))))))))))) + + +(** val str : char list **) + +let str = + 'T'::('h'::('i'::('s'::(' '::('i'::('s'::(' '::('a'::(' '::('s'::('t'::('r'::('i'::('n'::('g'::[]))))))))))))))) +(** val str : string **) + +let str = + "This is a string" +str :: Prelude.String +str = + "This is a string" + + diff --git a/test-suite/output/ExtractionString.v b/test-suite/output/ExtractionString.v new file mode 100644 index 0000000000..e4b9d22b38 --- /dev/null +++ b/test-suite/output/ExtractionString.v @@ -0,0 +1,25 @@ +Require Import String Extraction. + +Definition str := "This is a string"%string. + +(* Raw extraction of strings, in OCaml *) +Extraction Language OCaml. +Extraction str. + +(* Raw extraction of strings, in Haskell *) +Extraction Language Haskell. +Extraction str. + +(* Extraction to char list, in OCaml *) +Require Import ExtrOcamlString. +Extraction Language OCaml. +Extraction str. + +(* Extraction to native strings, in OCaml *) +Require Import ExtrOcamlNativeString. +Extraction str. + +(* Extraction to native strings, in Haskell *) +Require Import ExtrHaskellString. +Extraction Language Haskell. +Extraction str. diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out index 6879cbc3c2..60bc9cbf55 100644 --- a/test-suite/output/Fixpoint.out +++ b/test-suite/output/Fixpoint.out @@ -1,8 +1,8 @@ -fix F (A B : Set) (f : A -> B) (l : list A) {struct l} : -list B := match l with - | nil => nil - | a :: l0 => f a :: F A B f l0 - end +fix F (A B : Set) (f : A -> B) (l : list A) {struct l} : list B := + match l with + | nil => nil + | a :: l0 => f a :: F A B f l0 + end : forall A B : Set, (A -> B) -> list A -> list B let fix f (m : nat) : nat := match m with | 0 => 0 diff --git a/test-suite/output/Naming.out b/test-suite/output/Naming.out index c142d28ebe..0a989646cf 100644 --- a/test-suite/output/Naming.out +++ b/test-suite/output/Naming.out @@ -61,3 +61,18 @@ H : a = 0 -> forall a : nat, a = 0 ============================ a = 0 +File "stdin", line 101, characters 47-48: +Warning: Ignoring implicit binder declaration in unexpected position. +[unexpected-implicit-declaration,syntax] +File "stdin", line 105, characters 36-37: +Warning: Ignoring implicit binder declaration in unexpected position. +[unexpected-implicit-declaration,syntax] +File "stdin", line 106, characters 34-35: +Warning: Ignoring implicit binder declaration in unexpected position. +[unexpected-implicit-declaration,syntax] +File "stdin", line 112, characters 22-23: +Warning: Ignoring implicit binder declaration in unexpected position. +[unexpected-implicit-declaration,syntax] +File "stdin", line 112, characters 30-31: +Warning: Ignoring implicit binder declaration in unexpected position. +[unexpected-implicit-declaration,syntax] diff --git a/test-suite/output/Naming.v b/test-suite/output/Naming.v index 7f3b332d7d..610fa48c0c 100644 --- a/test-suite/output/Naming.v +++ b/test-suite/output/Naming.v @@ -90,3 +90,25 @@ apply H with (a:=a). (* test compliance with printing *) Abort. End A. + +Module B. + +(* Check valid/invalid implicit arguments *) +Definition f1 {x} (y:forall {x}, x=0) := x+0. +Definition f2 := (((fun x => 0):forall {x:nat}, nat), 0). +Definition f3 := fun {x} (y:forall {x}, x=0) => x+0. + +Definition g1 {x} := match x with true => fun {x:bool} => x | false => fun x:bool => x end. +(* TODO: do not ignore the implicit here *) +Definition g2 '(x,y) {z} := x+y+z. + +Definition h1 := fun x:nat => (fun {x} => x) 0. +Definition h2 := let g := forall {y}, y=0 in g. + +Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity, + format "'[ ' '[ ' ∀ x .. y ']' , '/' P ']'") : type_scope. + +Definition l1 := ∀ {x:nat} {y:nat}, x=0. + +End B. diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 94b86fc222..b870fa6f6f 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -137,3 +137,71 @@ end = p : forall x : nat, x = x -> Prop bar 0 : nat +let k := rew [P] p in v in k + : P y +let k := rew [P] p in v in k + : P y +let k := rew <- [P] p in v' in k + : P x +let k := rew [P] p in v in k + : P y +let k := rew [P] p in v in k + : P y +let k := rew <- [P] p in v' in k + : P x +let k := rew [fun y : A => P y] p in v in k + : P y +let k := rew [fun y : A => P y] p in v in k + : P y +let k := rew <- [fun y : A => P y] p in v' in k + : P x +let k := rew [fun y : A => P y] p in v in k + : P y +let k := rew [fun y : A => P y] p in v in k + : P y +let k := rew <- [fun y : A => P y] p in v' in k + : P x +let k := rew dependent [P] p in v in k + : P y p +let k := rew dependent [P] p in v in k + : P y p +let k := rew dependent <- [P'] p in v' in k + : P' x (eq_sym p) +let k := rew dependent [P] p in v in k + : P y p +let k := rew dependent [P] p in v in k + : P y p +let k := rew dependent <- [P'] p in v' in k + : P' x (eq_sym p) +let k := rew dependent [P] p in v in k + : P y p +let k := rew dependent [P] p in v in k + : P y p +let k := rew dependent <- [P'] p in v' in k + : P' x (eq_sym p) +let k := rew dependent [fun y p => id (P y p)] p in v in k + : P y p +let k := rew dependent [fun y p => id (P y p)] p in v in k + : P y p +let k := rew dependent <- [fun y0 p => id (P' y0 p)] p in v' in k + : P' x (eq_sym p) +let k := rew dependent [P] p in v in k + : P y p +let k := rew dependent [P] p in v in k + : P y p +let k := rew dependent <- [P'] p in v' in k + : P' x (eq_sym p) +let k := rew dependent [fun y p0 => id (P y p0)] p in v in k + : P y p +let k := rew dependent [fun y p0 => id (P y p0)] p in v in k + : P y p +let k := rew dependent <- [fun y0 p0 => id (P' y0 p0)] p in v' in k + : P' x (eq_sym p) +rew dependent [P] p in v + : P y p +rew dependent <- [P'] p in v' + : P' x (eq_sym p) +rew dependent [fun a x => id (P a x)] p in v + : id (P y p) +rew dependent <- [fun a p' => id (P' a p')] p in v' + : id (P' x (eq_sym p)) diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index adab324cf0..7d2f1e9ba8 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -251,11 +251,11 @@ Notation NONE := None. Check (fun x => match x with SOME x => x | NONE => 0 end). Notation NONE2 := (@None _). -Notation SOME2 := (@Some _). +Notation SOME2 := (@Some _). Check (fun x => match x with SOME2 x => x | NONE2 => 0 end). Notation NONE3 := @None. -Notation SOME3 := @Some. +Notation SOME3 := @Some. Check (fun x => match x with SOME3 _ x => x | NONE3 _ => 0 end). Notation "a :'" := (cons a) (at level 12). @@ -300,3 +300,61 @@ Definition bar (a b : nat) := plus a b. Notation "" := A (format "", only printing). Check (bar A 0). End M. + +(* Check eq notations *) +Module EqNotationsCheck. + Import EqNotations. + Section nd. + Context (A : Type) (x : A) (P : A -> Type) + (y : A) (p : x = y) (v : P x) (v' : P y). + + Check let k : P y := rew p in v in k. + Check let k : P y := rew -> p in v in k. + Check let k : P x := rew <- p in v' in k. + Check let k : P y := rew [P] p in v in k. + Check let k : P y := rew -> [P] p in v in k. + Check let k : P x := rew <- [P] p in v' in k. + Check let k : P y := rew [fun y => P y] p in v in k. + Check let k : P y := rew -> [fun y => P y] p in v in k. + Check let k : P x := rew <- [fun y => P y] p in v' in k. + Check let k : P y := rew [fun (y : A) => P y] p in v in k. + Check let k : P y := rew -> [fun (y : A) => P y] p in v in k. + Check let k : P x := rew <- [fun (y : A) => P y] p in v' in k. + End nd. + Section dep. + Context (A : Type) (x : A) (P : forall y, x = y -> Type) + (y : A) (p : x = y) (P' : forall x, y = x -> Type) + (v : P x eq_refl) (v' : P' y eq_refl). + + Check let k : P y p := rew dependent p in v in k. + Check let k : P y p := rew dependent -> p in v in k. + Check let k : P' x (eq_sym p) := rew dependent <- p in v' in k. + Check let k : P y p := rew dependent [P] p in v in k. + Check let k : P y p := rew dependent -> [P] p in v in k. + Check let k : P' x (eq_sym p) := rew dependent <- [P'] p in v' in k. + Check let k : P y p := rew dependent [fun y p => P y p] p in v in k. + Check let k : P y p := rew dependent -> [fun y p => P y p] p in v in k. + Check let k : P' x (eq_sym p) := rew dependent <- [fun y p => P' y p] p in v' in k. + Check let k : P y p := rew dependent [fun y p => id (P y p)] p in v in k. + Check let k : P y p := rew dependent -> [fun y p => id (P y p)] p in v in k. + Check let k : P' x (eq_sym p) := rew dependent <- [fun y p => id (P' y p)] p in v' in k. + Check let k : P y p := rew dependent [(fun (y : A) (p : x = y) => P y p)] p in v in k. + Check let k : P y p := rew dependent -> [(fun (y : A) (p : x = y) => P y p)] p in v in k. + Check let k : P' x (eq_sym p) := rew dependent <- [(fun (x : A) (p : y = x) => P' x p)] p in v' in k. + Check let k : P y p := rew dependent [(fun (y : A) (p : x = y) => id (P y p))] p in v in k. + Check let k : P y p := rew dependent -> [(fun (y : A) (p : x = y) => id (P y p))] p in v in k. + Check let k : P' x (eq_sym p) := rew dependent <- [(fun (x : A) (p : y = x) => id (P' x p))] p in v' in k. + Check match p as x in _ = a return P a x with + | eq_refl => v + end. + Check match eq_sym p as p' in _ = a return P' a p' with + | eq_refl => v' + end. + Check match p as x in _ = a return id (P a x) with + | eq_refl => v + end. + Check match eq_sym p as p' in _ = a return id (P' a p') with + | eq_refl => v' + end. + End dep. +End EqNotationsCheck. diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index aeebc0f98b..839df99ea7 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -219,8 +219,8 @@ Check exists_true '(x,y) (u:=0) '(z,t), x+y=0/\z+t=0. Module G. Generalizable Variables A R. Class Reflexive {A:Type} (R : A->A->Prop) := reflexivity : forall x : A, R x x. -Check exists_true `{Reflexive A R}, forall x, R x x. -Check exists_true x `{Reflexive A R} y, x+y=0 -> forall z, R z z. +Check exists_true `(Reflexive A R), forall x, R x x. +Check exists_true x `(Reflexive A R) y, x+y=0 -> forall z, R z z. End G. (* Allows recursive patterns for binders to be associative on the left *) diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 799d310fa7..f65696e464 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -4,11 +4,11 @@ Entry constr:myconstr is [ "6" RIGHTA [ ] | "5" RIGHTA - [ SELF; "+"; NEXT ] + [ SELF; "+"; NEXT ] | "4" RIGHTA - [ SELF; "*"; NEXT ] + [ SELF; "*"; NEXT ] | "3" RIGHTA - [ "<"; constr:operconstr LEVEL "10"; ">" ] ] + [ "<"; constr:operconstr LEVEL "10"; ">" ] ] [< b > + < b > * < 2 >] : nat @@ -63,3 +63,11 @@ fun '{| |} => true : R -> bool b = a : Prop +The command has indeed failed with message: +The format is not the same on the right- and left-hand sides of the special token "..". +The command has indeed failed with message: +The format is not the same on the right- and left-hand sides of the special token "..". +The command has indeed failed with message: +The format is not the same on the right- and left-hand sides of the special token "..". +The command has indeed failed with message: +The format is not the same on the right- and left-hand sides of the special token "..". diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 26c7840a16..4de6ce19b4 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -158,3 +158,29 @@ Check b = a. End Test. End L. + +Module M. + +(* Accept boxes around the end variables of a recursive notation (if equal boxes) *) + +Notation " {@ T1 ; T2 ; .. ; Tn } " := + (and T1 (and T2 .. (and Tn True)..)) + (format "'[v' {@ '[' T1 ']' ; '//' '[' T2 ']' ; '//' .. ; '//' '[' Tn ']' } ']'"). + +Fail Notation " {@ T1 ; T2 ; .. ; Tn } " := + (and T1 (and T2 .. (and Tn True)..)) + (format "'[v' {@ '[' T1 ']' ; '//' '[' T2 ']' ; '//' .. ; '//' '[' Tn ']' } ']'"). + +Fail Notation " {@ T1 ; T2 ; .. ; Tn } " := + (and T1 (and T2 .. (and Tn True)..)) + (format "'[v' {@ '[' T1 ']' ; '//' '[' T2 ']' ; '//' .. ; '//' '[v' Tn ']' } ']'"). + +Fail Notation " {@ T1 ; T2 ; .. ; Tn } " := + (and T1 (and T2 .. (and Tn True)..)) + (format "'[v' {@ '[' T1 ']' ; '//' '[' T2 ']' ; '//' .. ; '//' '[' Tn ']' } ']'"). + +Fail Notation " {@ T1 ; T2 ; .. ; Tn } " := + (and T1 (and T2 .. (and Tn True)..)) + (format "'[v' {@ '[' T1 ']' ; '//' '[' T2 ']' ; '//' .. ; '//' '[' Tn ']' } ']'"). + +End M. diff --git a/test-suite/output/Notations5.out b/test-suite/output/Notations5.out new file mode 100644 index 0000000000..83dd2f40fb --- /dev/null +++ b/test-suite/output/Notations5.out @@ -0,0 +1,248 @@ +p 0 0 true + : 0 = 0 /\ true = true +p 0 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +p 0 + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +p 0 0 (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +p 0 0 (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +p (A:=nat) + : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b +p (A:=nat) + : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b +@p nat 0 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b +@p + : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b +p 0 0 + : forall b : bool, 0 = 0 /\ b = b +p + : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b +p 0 0 true + : 0 = 0 /\ true = true +p 0 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +p 0 + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +p 0 0 + : forall b : bool, 0 = 0 /\ b = b +p 0 0 + : forall b : bool, 0 = 0 /\ b = b +p + : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b +p + : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b +@p nat 0 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b +@p + : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b +f x true + : 0 = 0 /\ true = true +f x (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +f x (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +@f nat + : forall a1 a2 : nat, + T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b +f (a1:=0) (a2:=0) + : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b +f (a1:=0) (a2:=0) + : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b +@f + : forall (A : Type) (a1 a2 : A), + T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b +f + : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b +x.(f) true + : 0 = 0 /\ true = true +x.(f) (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +x.(f) (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +@f nat + : forall a1 a2 : nat, + T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b +f (a1:=0) (a2:=0) + : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b +f (a1:=0) (a2:=0) + : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b +@f + : forall (A : Type) (a1 a2 : A), + T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b +f + : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b +p + : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b +where +?A : [ |- Type] +p + : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b +where +?A : [ |- Type] +u + : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b +u + : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b +p 0 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +p 0 0 + : forall b : bool, 0 = 0 /\ b = b +@p nat 0 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b +@p nat 0 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b +u + : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b +where +?A : [ |- Type] +u + : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b +u + : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b +u + : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b +where +?A : [ |- Type] +u 0 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +u 0 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +@u nat 0 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b +@u nat 0 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b +u 0 0 true + : 0 = 0 /\ true = true +u 0 0 true + : 0 = 0 /\ true = true +v + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +v 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +v 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +v 0 (B:=bool) true + : 0 = 0 /\ true = true +v + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +@v 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b +@v 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b +v 0 (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +v + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +v 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +v 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +v 0 (B:=bool) true + : 0 = 0 /\ true = true +v + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +@v 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b +@v 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b +v 0 (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +## + : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b +where +?A : [ |- Type] +## + : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b +where +?A : [ |- Type] +## 0 + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +## 0 + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +## 0 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +## 0 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +## 0 0 (B:=bool) true + : 0 = 0 /\ true = true +## 0 0 (B:=bool) true + : 0 = 0 /\ true = true +## 0 0 (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +## 0 0 (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +p + : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b +where +?A : [ |- Type] +## + : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b +## + : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b +p 0 + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +p 0 + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +@p nat 0 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b +p 0 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +p 0 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +p 0 0 (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +p 0 0 true + : 0 = 0 /\ true = true +## 0 + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +## 0 + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +## 0 0 (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +## 0 0 (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +## 0 0 (B:=bool) true + : 0 = 0 /\ true = true +## 0 0 (B:=bool) true + : 0 = 0 /\ true = true +## 0 + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +## 0 + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +## 0 0 (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +## 0 0 (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +## 0 0 (B:=bool) true + : 0 = 0 /\ true = true +## 0 0 (B:=bool) true + : 0 = 0 /\ true = true diff --git a/test-suite/output/Notations5.v b/test-suite/output/Notations5.v new file mode 100644 index 0000000000..b3bea929ba --- /dev/null +++ b/test-suite/output/Notations5.v @@ -0,0 +1,340 @@ +Module AppliedTermsPrinting. + +(* Test different printing paths for applied terms *) + + Module InferredGivenImplicit. + Set Implicit Arguments. + Set Maximal Implicit Insertion. + + Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b. + + Check p 0 0 true. + (* p 0 0 true *) + Check p 0 0. + (* p 0 0 *) + Check p 0. + (* p 0 *) + Check @p _ 0 0 bool. + (* p 0 0 (B:=bool) *) + Check p 0 0 (B:=bool). + (* p 0 0 (B:=bool) *) + Check @p nat. + (* p (A:=nat) *) + Check p (A:=nat). + (* p (A:=nat) *) + Check @p _ 0 0. + (* @p nat 0 0 *) + Check @p. + (* @p *) + + Unset Printing Implicit Defensive. + Check @p _ 0 0 bool. + (* p 0 0 *) + Check @p nat. + (* p *) + Set Printing Implicit Defensive. + End InferredGivenImplicit. + + Module ManuallyGivenImplicit. + Axiom p : forall {A} (a1 a2:A) {B} (b:B), a1 = a2 /\ b = b. + + Check p 0 0 true. + (* p 0 0 true *) + Check p 0 0. + (* p 0 0 *) + Check p 0. + (* p 0 *) + Check @p _ 0 0 bool. + (* p 0 0 *) + Check p 0 0 (B:=bool). + (* p 0 0 *) + Check @p nat. + (* p *) + Check p (A:=nat). + (* p *) + Check @p _ 0 0. + (* @p nat 0 0 *) + Check @p. + (* @p *) + + End ManuallyGivenImplicit. + + Module ProjectionWithImplicits. + Set Implicit Arguments. + Set Maximal Implicit Insertion. + + Record T {A} (a1 a2:A) := { f : forall B (b:B), a1 = a2 /\ b = b }. + Parameter x : T 0 0. + Check f x true. + (* f x true *) + Check @f _ _ _ x bool. + (* f x (B:=bool) *) + Check f x (B:=bool). + (* f x (B:=bool) *) + Check @f nat. + (* @f nat *) + Check @f _ 0 0. + (* f (a1:=0) (a2:=0) *) + Check f (a1:=0) (a2:=0). + (* f (a1:=0) (a2:=0) *) + Check @f. + (* @f *) + + Unset Printing Implicit Defensive. + Check f (a1:=0) (a2:=0). + (* f *) + Set Printing Implicit Defensive. + + Set Printing Projections. + + Check x.(f) true. + (* x.(f) true *) + Check x.(@f _ _ _) bool. + (* x.(f) (B:=bool) *) + Check x.(f) (B:=bool). + (* x.(f) (B:=bool) *) + Check @f nat. + (* @f nat *) + Check @f _ 0 0. + (* f (a1:=0) (a2:=0) *) + Check f (a1:=0) (a2:=0). + (* f (a1:=0) (a2:=0) *) + Check @f. + (* @f *) + + Unset Printing Implicit Defensive. + Check f (a1:=0) (a2:=0). + (* f *) + + End ProjectionWithImplicits. + + Module AtAbbreviationForApplicationHead. + + Axiom p : forall {A} (a1 a2:A) {B} (b:B), a1 = a2 /\ b = b. + + Notation u := @p. + + Check u _. + (* p *) + Check p. + (* p *) + Check @p. + (* u *) + Check u. + (* u *) + Check p 0 0. + (* p 0 0 *) + Check u nat 0 0 bool. + (* p 0 0 -- WEAKNESS should ideally be (B:=bool) *) + Check u nat 0 0. + (* @p nat 0 0 *) + Check @p nat 0 0. + (* @p nat 0 0 *) + + End AtAbbreviationForApplicationHead. + + Module AbbreviationForApplicationHead. + + Set Implicit Arguments. + Set Maximal Implicit Insertion. + + Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b. + + Notation u := p. + + Check p. + (* u *) + Check @p. + (* u -- BUG *) + Check @u. + (* u -- BUG *) + Check u. + (* u *) + Check p 0 0. + (* u 0 0 *) + Check u 0 0. + (* u 0 0 *) + Check @p nat 0 0. + (* @u nat 0 0 *) + Check @u nat 0 0. + (* @u nat 0 0 *) + Check p 0 0 true. + (* u 0 0 true *) + Check u 0 0 true. + (* u 0 0 true *) + + End AbbreviationForApplicationHead. + + Module AtAbbreviationForPartialApplication. + + Set Implicit Arguments. + Set Maximal Implicit Insertion. + + Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b. + + Notation v := (@p _ 0). + + Check v. + (* v *) + Check p 0 0. + (* v 0 *) + Check v 0. + (* v 0 *) + Check v 0 true. + (* v 0 (B:=bool) true -- BUG *) + Check @p nat 0. + (* v *) + Check @p nat 0 0. + (* @v 0 *) + Check @v 0. + (* @v 0 *) + Check @p nat 0 0 bool. + (* v 0 (B:=bool) *) + + End AtAbbreviationForPartialApplication. + + Module AbbreviationForPartialApplication. + + Set Implicit Arguments. + Set Maximal Implicit Insertion. + + Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b. + + Notation v := (p 0). + + Check v. + (* v *) + Check p 0 0. + (* v 0 *) + Check v 0. + (* v 0 *) + Check v 0 true. + (* v 0 (B:=bool) true -- BUG *) + Check @p nat 0. + (* v *) + Check @p nat 0 0. + (* @v 0 *) + Check @v 0. + (* @v 0 *) + Check @p nat 0 0 bool. + (* v 0 (B:=bool) *) + + End AbbreviationForPartialApplication. + + Module NotationForHeadApplication. + + Set Implicit Arguments. + Set Maximal Implicit Insertion. + + Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b. + + Notation "##" := p (at level 0). + + Check p. + (* ## *) + Check ##. + (* ## *) + Check p 0. + (* ## 0 *) + Check ## 0. + (* ## 0 *) + Check p 0 0. + (* ## 0 0 *) + Check ## 0 0. + (* ## 0 0 *) + Check p 0 0 true. + (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *) + Check ## 0 0 true. + (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *) + Check p 0 0 (B:=bool). + (* ## 0 0 (B:=bool) *) + Check ## 0 0 (B:=bool). + (* ## 0 0 (B:=bool) *) + + End NotationForHeadApplication. + + Module AtNotationForHeadApplication. + + Set Implicit Arguments. + Set Maximal Implicit Insertion. + + Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b. + + Notation "##" := @p (at level 0). + + Check p. + (* p *) + Check @p. + (* ## *) + Check ##. + (* ## *) + Check p 0. + (* p 0 -- why not "## nat 0" *) + Check ## nat 0. + (* p 0 *) + Check ## nat 0 0. + (* @p nat 0 0 *) + Check p 0 0. + (* p 0 0 *) + Check ## nat 0 0 _. + (* p 0 0 *) + Check ## nat 0 0 bool. + (* p 0 0 (B:=bool) *) + Check ## nat 0 0 bool true. + (* p 0 0 true *) + + End AtNotationForHeadApplication. + + Module NotationForPartialApplication. + + Set Implicit Arguments. + Set Maximal Implicit Insertion. + + Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b. + + Notation "## q" := (p q) (at level 0, q at level 0). + + Check p 0. + (* ## 0 *) + Check ## 0. + (* ## 0 *) + (* Check ## 0 0. *) + (* Anomaly *) + Check p 0 0 (B:=bool). + (* ## 0 0 (B:=bool) *) + Check ## 0 0 bool. + (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *) + Check p 0 0 true. + (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *) + Check ## 0 0 bool true. + (* ## 0 0 (B:=bool) true -- INCONSISTENT parsing/printing + BUG B should not be displayed *) + + End NotationForPartialApplication. + + Module AtNotationForPartialApplication. + + Set Implicit Arguments. + Set Maximal Implicit Insertion. + + Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b. + + Notation "## q" := (@p _ q) (at level 0, q at level 0). + + Check p 0. + (* ## 0 *) + Check ## 0. + (* ## 0 *) + (* Check ## 0 0. *) + (* Anomaly *) + Check p 0 0 (B:=bool). + (* ## 0 0 (B:=bool) *) + Check ## 0 0 bool. + (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *) + Check p 0 0 true. + (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *) + Check ## 0 0 bool true. + (* ## 0 0 (B:=bool) true -- INCONSISTENCY parsing/printing + BUG B should not be displayed *) + + End AtNotationForPartialApplication. + +End AppliedTermsPrinting. diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out index 3f4d5ef58c..190c34262f 100644 --- a/test-suite/output/PrintAssumptions.out +++ b/test-suite/output/PrintAssumptions.out @@ -3,6 +3,10 @@ foo : nat Axioms: foo : nat Axioms: +bli : Type +Axioms: +bli : Type +Axioms: extensionality : forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g Axioms: diff --git a/test-suite/output/PrintAssumptions.v b/test-suite/output/PrintAssumptions.v index 3d4dfe603d..4c980fddba 100644 --- a/test-suite/output/PrintAssumptions.v +++ b/test-suite/output/PrintAssumptions.v @@ -30,6 +30,21 @@ Module P := N M. Print Assumptions M.bar. (* Should answer: foo *) Print Assumptions P.bar. (* Should answer: foo *) +(* Print Assumptions used empty instances on polymorphic inductives *) +Module Poly. + + Set Universe Polymorphism. + Axiom bli : Type. + + Definition bla := bli -> bli. + + Inductive blo : bli -> Type := . + + Print Assumptions bla. + Print Assumptions blo. + +End Poly. + (* The original test-case of the bug-report *) diff --git a/test-suite/output/QArithSyntax.out b/test-suite/output/QArithSyntax.out new file mode 100644 index 0000000000..6bc04f1cef --- /dev/null +++ b/test-suite/output/QArithSyntax.out @@ -0,0 +1,14 @@ +eq_refl : 102e-2 = 102e-2 + : 102e-2 = 102e-2 +eq_refl : 102e-1 = 102e-1 + : 102e-1 = 102e-1 +eq_refl : 1020 = 1020 + : 1020 = 1020 +eq_refl : 102 = 102 + : 102 = 102 +eq_refl : 102e-2 = 102e-2 + : 102e-2 = 102e-2 +eq_refl : -1e-4 = -1e-4 + : -1e-4 = -1e-4 +eq_refl : -50e-2 = -50e-2 + : -50e-2 = -50e-2 diff --git a/test-suite/success/QArithSyntax.v b/test-suite/output/QArithSyntax.v index 2f2ee0134a..2f2ee0134a 100644 --- a/test-suite/success/QArithSyntax.v +++ b/test-suite/output/QArithSyntax.v diff --git a/test-suite/output/RealSyntax.out b/test-suite/output/RealSyntax.out index e6f7556d96..2d877bd813 100644 --- a/test-suite/output/RealSyntax.out +++ b/test-suite/output/RealSyntax.out @@ -2,3 +2,17 @@ : R (-31)%R : R +eq_refl : 102e-2 = 102e-2 + : 102e-2 = 102e-2 +eq_refl : 102e-1 = 102e-1 + : 102e-1 = 102e-1 +eq_refl : 102e1 = 102e1 + : 102e1 = 102e1 +eq_refl : 102 = 102 + : 102 = 102 +eq_refl : 102e-2 = 102e-2 + : 102e-2 = 102e-2 +eq_refl : -1e-4 = -1e-4 + : -1e-4 = -1e-4 +eq_refl : -50e-2 = -50e-2 + : -50e-2 = -50e-2 diff --git a/test-suite/output/RealSyntax.v b/test-suite/output/RealSyntax.v index 44e8c7a50c..cb3bce70d4 100644 --- a/test-suite/output/RealSyntax.v +++ b/test-suite/output/RealSyntax.v @@ -1,3 +1,25 @@ Require Import Reals.Rdefinitions. Check 32%R. Check (-31)%R. + +Open Scope R_scope. + +Check (eq_refl : 1.02 = IZR 102 / IZR (Z.pow_pos 10 2)). +Check (eq_refl : 1.02e1 = IZR 102 / IZR (Z.pow_pos 10 1)). +Check (eq_refl : 1.02e+03 = IZR 102 * IZR (Z.pow_pos 10 1)). +Check (eq_refl : 1.02e+02 = IZR 102). +Check (eq_refl : 10.2e-1 = 1.02). +Check (eq_refl : -0.0001 = IZR (-1) / IZR (Z.pow_pos 10 4)). +Check (eq_refl : -0.50 = IZR (-50) / IZR (Z.pow_pos 10 2)). + +Require Import Reals. + +Goal 254e3 = 2540 * 10 ^ 2. +ring. +Qed. + +Require Import Psatz. + +Goal 254e3 = 2540 * 10 ^ 2. +lra. +Qed. diff --git a/test-suite/prerequisite/ssr_mini_mathcomp.v b/test-suite/prerequisite/ssr_mini_mathcomp.v index d293dc0533..048fb3b027 100644 --- a/test-suite/prerequisite/ssr_mini_mathcomp.v +++ b/test-suite/prerequisite/ssr_mini_mathcomp.v @@ -65,7 +65,7 @@ Proof. by []. Qed. Lemma eqP T : Equality.axiom (@eq_op T). Proof. by case: T => ? []. Qed. -Arguments eqP [T x y]. +Arguments eqP {T x y}. Delimit Scope eq_scope with EQ. Open Scope eq_scope. @@ -345,7 +345,7 @@ Proof. by []. Qed. End SubEqType. -Arguments val_eqP [T P sT x y]. +Arguments val_eqP {T P sT x y}. Prenex Implicits val_eqP. Notation "[ 'eqMixin' 'of' T 'by' <: ]" := (SubEqMixin _ : Equality.class_of T) @@ -386,7 +386,7 @@ Qed. Canonical nat_eqMixin := EqMixin eqnP. Canonical nat_eqType := Eval hnf in EqType nat nat_eqMixin. -Arguments eqnP [x y]. +Arguments eqnP {x y}. Prenex Implicits eqnP. Coercion nat_of_bool (b : bool) := if b then 1 else 0. diff --git a/test-suite/success/CanonicalStructure.v b/test-suite/success/CanonicalStructure.v index e6d674c1e6..88702a6e80 100644 --- a/test-suite/success/CanonicalStructure.v +++ b/test-suite/success/CanonicalStructure.v @@ -51,3 +51,22 @@ Fail Check (refl_equal _ : l _ = x2). Check s0. Check s1. Check s2. + +Section Y. + Let s3 := MKL x3. + Canonical Structure s3. + Check (refl_equal _ : l _ = x3). +End Y. +Fail Check (refl_equal _ : l _ = x3). +Fail Check s3. + +Section V. + #[canonical] Let s3 := MKL x3. + Check (refl_equal _ : l _ = x3). +End V. + +Section W. + #[canonical, local] Definition s2' := MKL x2. + Check (refl_equal _ : l _ = x2). +End W. +Fail Check (refl_equal _ : l _ = x2). diff --git a/test-suite/success/CompatOldOldFlag.v b/test-suite/success/CompatOldOldFlag.v deleted file mode 100644 index dd259988ac..0000000000 --- a/test-suite/success/CompatOldOldFlag.v +++ /dev/null @@ -1,6 +0,0 @@ -(* -*- coq-prog-args: ("-compat" "8.9") -*- *) -(** Check that the current-minus-three compatibility flag actually requires the relevant modules. *) -Import Coq.Compat.Coq812. -Import Coq.Compat.Coq811. -Import Coq.Compat.Coq810. -Import Coq.Compat.Coq89. diff --git a/test-suite/success/Generalization.v b/test-suite/success/Generalization.v index de34e007d2..df729588f4 100644 --- a/test-suite/success/Generalization.v +++ b/test-suite/success/Generalization.v @@ -11,4 +11,10 @@ Admitted. Print a_eq_b. +Require Import Morphisms. +Class Equiv A := equiv : A -> A -> Prop. +Class Setoid A `{Equiv A} := setoid_equiv:> Equivalence (equiv). + +Lemma vcons_proper A `[Equiv A] `[!Setoid A] (x : True) : True. +Admitted. diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v index b16e4a1186..e68040e4d4 100644 --- a/test-suite/success/ImplicitArguments.v +++ b/test-suite/success/ImplicitArguments.v @@ -1,3 +1,15 @@ + +Axiom foo : forall (x y z t : nat), nat. + +Arguments foo {_} _ [z] t. +Check (foo 1). +Arguments foo {_} _ {z} {t}. +Fail Arguments foo {_} _ [z] {t}. +Check (foo 1). + +Definition foo1 [m] n := n + m. +Check (foo1 1). + Inductive vector {A : Type} : nat -> Type := | vnil : vector 0 | vcons : A -> forall {n'}, vector n' -> vector (S n'). @@ -33,3 +45,11 @@ Abort. Inductive A {P:forall m {n}, n=m -> Prop} := C : P 0 eq_refl -> A. Inductive B (P:forall m {n}, n=m -> Prop) := D : P 0 eq_refl -> B P. + +Inductive A' {P:forall m [n], n=m -> Prop} := C' : P 0 eq_refl -> A'. +Inductive A'' [P:forall m {n}, n=m -> Prop] (b : bool):= C'' : P 0 eq_refl -> A'' b. +Inductive A''' (P:forall m [n], n=m -> Prop) (b : bool):= C''' : P 0 eq_refl -> A''' P b. + +Definition F (id: forall [A] [x : A], A) := id. +Definition G := let id := (fun [A] (x : A) => x) in id. +Fail Definition G' := let id := (fun {A} (x : A) => x) in id. diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index c2130995fc..4b2d4457bf 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -71,7 +71,7 @@ CoInductive LList (A : Set) : Set := | LNil : LList A | LCons : A -> LList A -> LList A. -Arguments LNil [A]. +Arguments LNil {A}. Inductive Finite (A : Set) : LList A -> Prop := | Finite_LNil : Finite LNil @@ -204,3 +204,19 @@ End NonRecLetIn. Fail Inductive foo (T : Type) : let T := Type in T := { r : forall x : T, x = x }. + +Module Discharge. + (* discharge test *) + Section S. + Let x := Prop. + Inductive foo : x := bla : foo. + End S. + Check bla:foo. + + Section S. + Variables (A:Type). + (* ensure params are scanned for needed section variables even with template arity *) + #[universes(template)] Inductive bar (d:A) := . + End S. + Check @bar nat 0. +End Discharge. diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v index 1dbeaf3e1f..8297f54641 100644 --- a/test-suite/success/Inversion.v +++ b/test-suite/success/Inversion.v @@ -31,7 +31,7 @@ Inductive in_extension (I : Set) (r : rule I) : extension I -> Type := | in_first : forall e, in_extension r (add_rule r e) | in_rest : forall e r', in_extension r e -> in_extension r (add_rule r' e). -Arguments NL [I]. +Arguments NL {I}. Inductive super_extension (I : Set) (e : extension I) : extension I -> Type := diff --git a/test-suite/success/RealSyntax.v b/test-suite/success/RealSyntax.v deleted file mode 100644 index 2765200991..0000000000 --- a/test-suite/success/RealSyntax.v +++ /dev/null @@ -1,19 +0,0 @@ -Require Import Reals. -Open Scope R_scope. -Check (eq_refl : 1.02 = IZR 102 / IZR (Z.pow_pos 10 2)). -Check (eq_refl : 1.02e1 = IZR 102 / IZR (Z.pow_pos 10 1)). -Check (eq_refl : 1.02e+03 = IZR 102 * IZR (Z.pow_pos 10 1)). -Check (eq_refl : 1.02e+02 = IZR 102). -Check (eq_refl : 10.2e-1 = 1.02). -Check (eq_refl : -0.0001 = IZR (-1) / IZR (Z.pow_pos 10 4)). -Check (eq_refl : -0.5 = IZR (-5) / IZR (Z.pow_pos 10 1)). - -Goal 254e3 = 2540 * 10 ^ 2. -ring. -Qed. - -Require Import Psatz. - -Goal 254e3 = 2540 * 10 ^ 2. -lra. -Qed. diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v index 4fac798f76..15672eab7c 100644 --- a/test-suite/success/RecTutorial.v +++ b/test-suite/success/RecTutorial.v @@ -994,7 +994,7 @@ Qed. Arguments Vector.cons [A] _ [n]. -Arguments Vector.nil [A]. +Arguments Vector.nil {A}. Arguments Vector.hd [A n]. Arguments Vector.tl [A n]. @@ -1161,7 +1161,7 @@ infiniteproof map_iterate'. Qed. -Arguments LNil [A]. +Arguments LNil {A}. Lemma Lnil_not_Lcons : forall (A:Set)(a:A)(l:LList A), LNil <> (LCons a l). diff --git a/test-suite/success/Scheme.v b/test-suite/success/Scheme.v index 855f26698c..4b928007cf 100644 --- a/test-suite/success/Scheme.v +++ b/test-suite/success/Scheme.v @@ -25,3 +25,8 @@ Check myeq_rew_fwd_r_dep. Set Rewriting Schemes. Inductive myeq_true : bool -> Prop := myrefl_true : myeq_true true. Unset Rewriting Schemes. + +(* check that the scheme doesn't minimize itself into something non general *) +Polymorphic Inductive foo@{u v|u<=v} : Type@{u}:= . +Lemma bla@{u v|u < v} : foo@{u v} -> False. +Proof. induction 1. Qed. diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index ecaaedca53..59650d6822 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -114,9 +114,13 @@ Check h 0. Inductive I {A} (a:A) : forall {n:nat}, Prop := | C : I a (n:=0). +Inductive I' [A] (a:A) : forall [n:nat], n =0 -> Prop := + | C' : I' a eq_refl. + Inductive I2 (x:=0) : Prop := - | C2 {p:nat} : p = 0 -> I2. -Check C2 eq_refl. + | C2 {p:nat} : p = 0 -> I2 + | C2' [p:nat] : p = 0 -> I2. +Check C2' eq_refl. Inductive I3 {A} (x:=0) (a:A) : forall {n:nat}, Prop := | C3 : I3 a (n:=0). @@ -147,6 +151,7 @@ Set Warnings "syntax". (* Miscellaneous tests *) Check let f := fun {x:nat} y => y=true in f false. +Check let f := fun [x:nat] y => y=true in f false. (* Isn't the name "arg_1" a bit fragile, here? *) @@ -157,3 +162,23 @@ Check fun f : forall {_:nat}, nat => f (arg_1:=0). Set Warnings "+syntax". Check id (fun x => let f c {a} (b:a=a) := b in f true (eq_refl 0)). Set Warnings "syntax". + + +Axiom eq0le0 : forall (n : nat) (x : n = 0), n <= 0. +Variable eq0le0' : forall (n : nat) {x : n = 0}, n <= 0. +Axiom eq0le0'' : forall (n : nat) {x : n = 0}, n <= 0. +Definition eq0le0''' : forall (n : nat) {x : n = 0}, n <= 0. Admitted. +Fail Axiom eq0le0'''' : forall [n : nat] {x : n = 0}, n <= 0. + +Module TestUnnamedImplicit. + +Axiom foo : forall A, A -> A. + +Arguments foo {A} {_}. +Check foo (arg_2:=true) : bool. +Check foo : bool. + +Arguments foo {A} {x}. +Check foo (x:=true) : bool. + +End TestUnnamedImplicit. diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v index 1b04594290..1122b9fa34 100644 --- a/test-suite/success/specialize.v +++ b/test-suite/success/specialize.v @@ -109,28 +109,37 @@ match goal with H:_ |- _ => clear H end. match goal with H:_ |- _ => exact H end. Qed. -(* let ins should be supported in the type of the specialized hypothesis *) -Axiom foo: forall (m1 m2: nat), let n := 2 * m1 in m1 = m2 -> False. + +(* let ins should be supported int he type of the specialized hypothesis *) +Axiom foo: forall (m1:nat) (m2: nat), let n := 2 * m1 in (m1 = m2 -> False). Goal False. pose proof foo as P. assert (2 = 2) as A by reflexivity. + (* specialize P with (m2:= 2). *) specialize P with (1 := A). + match type of P with + | let n := 2 * 2 in False => idtac + | _ => fail "test failed" + end. assumption. Qed. (* Another more subtle test on letins: they should not interfere with foralls. *) -Goal forall (P: forall y:nat, - forall A (zz:A), - let a := zz in - let x := 1 in - forall n : y = x, - n = n), +Goal forall (P: forall a c:nat, + let b := c in + let d := 1 in + forall n : a = d, a = c+1), True. intros P. - specialize P with (zz := @eq_refl _ 2). + specialize P with (1:=eq_refl). + match type of P with + | forall c : nat, let f := c in let d := 1 in 1 = c + 1 => idtac + | _ => fail "test failed" + end. constructor. Qed. + (* Test specialize as *) Goal (forall x, x=0) -> 1=0. diff --git a/test-suite/success/uniform_inductive_parameters.v b/test-suite/success/uniform_inductive_parameters.v index 42236a5313..651247937d 100644 --- a/test-suite/success/uniform_inductive_parameters.v +++ b/test-suite/success/uniform_inductive_parameters.v @@ -1,13 +1,23 @@ +Module Att. + #[uniform] Inductive list (A : Type) := + | nil : list + | cons : A -> list -> list. + Check (list : Type -> Type). + Check (cons : forall A, A -> list A -> list A). +End Att. + Set Uniform Inductive Parameters. Inductive list (A : Type) := - | nil : list - | cons : A -> list -> list. +| 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. +| nil2 : list2 +| cons2 : A' -> list2 -> list2. Check (list2 : Type -> Type). Check (cons2 : forall A (A' := prod A A), A' -> list2 A -> list2 A). + +#[nonuniform] Inductive bla (n:nat) := c (_ : bla (S n)). diff --git a/test-suite/tools/update-compat/run.sh b/test-suite/tools/update-compat/run.sh index 61273c4f37..7ff5571ffb 100755 --- a/test-suite/tools/update-compat/run.sh +++ b/test-suite/tools/update-compat/run.sh @@ -6,4 +6,4 @@ SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )" # we assume that the script lives in test-suite/tools/update-compat/, # and that update-compat.py lives in dev/tools/ cd "${SCRIPT_DIR}/../../.." -dev/tools/update-compat.py --assert-unchanged --master || exit $? +dev/tools/update-compat.py --assert-unchanged --release || exit $? |