diff options
Diffstat (limited to 'test-suite')
52 files changed, 598 insertions, 94 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index b3a633e528..265c2eafa7 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -530,14 +530,16 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG) $(HIDE){ \ echo $(call log_intro,$<); \ true "extract effective user time"; \ - res=`$(coqc_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1 | sed "s/\r//g"`; \ + res=`$(coqc_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished .*transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1 | sed "s/\r//g"`; \ R=$$?; times; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ echo " $<...Error! (should be accepted)" ; \ + $(FAIL); \ elif [ "$$res" = "" ]; then \ echo $(log_failure); \ echo " $<...Error! (couldn't find a time measure)"; \ + $(FAIL); \ else \ true "express effective time in centiseconds"; \ resorig="$$res"; \ @@ -641,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/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_11321.v b/test-suite/bugs/closed/bug_11321.v new file mode 100644 index 0000000000..ce95280fb1 --- /dev/null +++ b/test-suite/bugs/closed/bug_11321.v @@ -0,0 +1,10 @@ +Require Import Cyclic63. + +Goal False. +Proof. +assert (4294967296 *c 2147483648 = WW 2 0)%int63 as H. + vm_cast_no_check (@eq_refl (zn2z int) (WW 2 0)%int63). +generalize (f_equal (zn2z_to_Z wB to_Z) H). +now rewrite mulc_WW_spec. +Fail Qed. +Abort. 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_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/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/findlib-package-unpacked/Makefile.local b/test-suite/coq-makefile/findlib-package-unpacked/Makefile.local new file mode 100644 index 0000000000..0f4a7d9954 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package-unpacked/Makefile.local @@ -0,0 +1 @@ +CAMLPKGS += -package foo diff --git a/test-suite/coq-makefile/findlib-package-unpacked/_CoqProject b/test-suite/coq-makefile/findlib-package-unpacked/_CoqProject new file mode 100644 index 0000000000..cbdb43f842 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package-unpacked/_CoqProject @@ -0,0 +1,10 @@ +-R src test +-R theories test +-I src + +src/test_plugin.mllib +src/test.mlg +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v diff --git a/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/META b/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/META new file mode 100644 index 0000000000..ff5f1c7c96 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/META @@ -0,0 +1,4 @@ +archive(byte)="foo.cma" +archive(native)="foo.cmxa" +linkopts="-linkall" +requires="str" diff --git a/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/Makefile b/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/Makefile new file mode 100644 index 0000000000..1615bfd067 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/Makefile @@ -0,0 +1,14 @@ +-include ../../Makefile.conf + +CO="$(COQMF_OCAMLFIND)" opt +CB="$(COQMF_OCAMLFIND)" ocamlc + +all: + $(CO) -c foolib.ml + $(CO) -a foolib.cmx -o foo.cmxa + $(CB) -c foolib.ml + $(CB) -a foolib.cmo -o foo.cma + $(CB) -c foo.mli # empty .mli file, to be understood + +clean: + rm -f *.cmo *.cma *.cmx *.cmxa *.cmi *.o *.a diff --git a/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/foo.mli b/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/foo.mli new file mode 100644 index 0000000000..e69de29bb2 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/foo.mli diff --git a/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/foolib.ml b/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/foolib.ml new file mode 100644 index 0000000000..81306fb89b --- /dev/null +++ b/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/foolib.ml @@ -0,0 +1,2 @@ +let foo () = + assert(Str.search_forward (Str.regexp "foo") "barfoobar" 0 = 3) diff --git a/test-suite/coq-makefile/findlib-package-unpacked/run.sh b/test-suite/coq-makefile/findlib-package-unpacked/run.sh new file mode 100755 index 0000000000..e53a7ed0f7 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package-unpacked/run.sh @@ -0,0 +1,20 @@ +#!/usr/bin/env bash + +. ../template/init.sh +mv src/test_plugin.mlpack src/test_plugin.mllib + +echo "let () = Foolib.foo ();;" >> src/test_aux.ml +export OCAMLPATH=$OCAMLPATH:$PWD/findlib +if which cygpath 2>/dev/null; then + # the only way I found to pass OCAMLPATH on win is to have it contain + # only one entry + OCAMLPATH=$(cygpath -w "$PWD"/findlib) + export OCAMLPATH +fi +make -C findlib/foo clean +coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf +cat Makefile.local +make -C findlib/foo +make +make byte 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 index 75b2a56169..fbd9c8bcba 100644 --- a/test-suite/failure/Template.v +++ b/test-suite/failure/Template.v @@ -1,4 +1,4 @@ -(* + Module TestUnsetTemplateCheck. Unset Template Check. @@ -15,18 +15,14 @@ Module TestUnsetTemplateCheck. (* 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 -*) + (* test discharge puts things in the right order (by using the + checker on the result) *) + Section S. + + Variables (A:Type) (a:A). + Inductive bb (B:Type) := BB : forall a', a = a' -> B -> bb B. + End S. + End TestUnsetTemplateCheck. -*) 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/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/Cases.out b/test-suite/output/Cases.out index e84ac85aa8..6976610b22 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -166,3 +166,15 @@ fun x : K => match x with : K -> nat The command has indeed failed with message: Pattern "S _, _" is redundant in this clause. +stray = +fun N : Tree => +match N with +| App (App Node (Node as strayvariable)) _ | + App (App Node (App Node _ as strayvariable)) _ | + App (App Node (App (App Node Node) (App _ _) as strayvariable)) _ | + App (App Node (App (App Node (App _ _)) _ as strayvariable)) _ | + App (App Node (App (App (App _ _) _) _ as strayvariable)) _ => + strayvariable +| _ => Node +end + : Tree -> Tree diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index a040b69b44..262ec2b677 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -222,3 +222,23 @@ 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. + +Module Bug11231. + +(* Missing dependency in computing if a clause is a default clause *) + +Inductive Tree: Set := +| Node : Tree +| App : Tree -> Tree -> Tree +. + +Definition stray N := +match N with +| App (App Node (App (App Node Node) Node)) _ => Node +| App (App Node strayvariable) _ => strayvariable +| _ => Node +end. + +Print stray. + +End Bug11231. 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/PrintCanonicalProjections.out b/test-suite/output/PrintCanonicalProjections.out new file mode 100644 index 0000000000..a4e2251440 --- /dev/null +++ b/test-suite/output/PrintCanonicalProjections.out @@ -0,0 +1,18 @@ +bool <- sort_eq ( bool_eqType ) +bool <- sort_TYPE ( bool_TYPE ) +nat <- sort_eq ( nat_eqType ) +nat <- sort_TYPE ( nat_TYPE ) +prod <- sort_eq ( prod_eqType ) +prod <- sort_TYPE ( prod_TYPE ) +sum <- sort_eq ( sum_eqType ) +sum <- sort_TYPE ( sum_TYPE ) +sum <- sort_TYPE ( sum_TYPE ) +prod <- sort_TYPE ( prod_TYPE ) +nat <- sort_TYPE ( nat_TYPE ) +bool <- sort_TYPE ( bool_TYPE ) +sum <- sort_eq ( sum_eqType ) +prod <- sort_eq ( prod_eqType ) +nat <- sort_eq ( nat_eqType ) +bool <- sort_eq ( bool_eqType ) +bool <- sort_TYPE ( bool_TYPE ) +bool <- sort_eq ( bool_eqType ) diff --git a/test-suite/output/PrintCanonicalProjections.v b/test-suite/output/PrintCanonicalProjections.v new file mode 100644 index 0000000000..808cdffe39 --- /dev/null +++ b/test-suite/output/PrintCanonicalProjections.v @@ -0,0 +1,46 @@ +Record TYPE := Pack_TYPE { sort_TYPE :> Type }. +Record eqType := Pack_eq { sort_eq :> Type; _ : sort_eq -> sort_eq -> bool }. + +Definition eq_op (T : eqType) : T -> T -> bool := + match T with Pack_eq _ op => op end. + +Definition bool_eqb b1 b2 := + match b1, b2 with + | false, false => true + | true, true => true + | _, _ => false + end. + +Canonical bool_TYPE := Pack_TYPE bool. +Canonical bool_eqType := Pack_eq bool bool_eqb. + +Canonical nat_TYPE := Pack_TYPE nat. +Canonical nat_eqType := Pack_eq nat Nat.eqb. + +Definition prod_eqb (T U : eqType) (x y : T * U) := + match x, y with + | (x1, x2), (y1, y2) => + andb (eq_op _ x1 y1) (eq_op _ x2 y2) + end. + +Canonical prod_TYPE (T U : TYPE) := Pack_TYPE (T * U). +Canonical prod_eqType (T U : eqType) := Pack_eq (T * U) (prod_eqb T U). + +Definition sum_eqb (T U : eqType) (x y : T + U) := + match x, y with + | inl x, inl y => eq_op _ x y + | inr x, inr y => eq_op _ x y + | _, _ => false + end. + +Canonical sum_TYPE (T U : TYPE) := Pack_TYPE (T + U). +Canonical sum_eqType (T U : eqType) := Pack_eq (T + U) (sum_eqb T U). + +Print Canonical Projections bool. +Print Canonical Projections nat. +Print Canonical Projections prod. +Print Canonical Projections sum. +Print Canonical Projections sort_TYPE. +Print Canonical Projections sort_eq. +Print Canonical Projections sort_TYPE bool. +Print Canonical Projections bool_eqType. 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/output/unification.out b/test-suite/output/unification.out new file mode 100644 index 0000000000..dfd755da61 --- /dev/null +++ b/test-suite/output/unification.out @@ -0,0 +1,11 @@ +The command has indeed failed with message: +In environment +x : T +T : Type +a : T +Unable to unify "T" with "?X@{x0:=x; x:=C a}" (cannot instantiate +"?X" because "T" is not in its scope: available arguments are +"x" "C a"). +The command has indeed failed with message: +The term "id" has type "ID" while it is expected to have type +"Type -> ?T" (cannot instantiate "?T" because "A" is not in its scope). diff --git a/test-suite/output/unification.v b/test-suite/output/unification.v new file mode 100644 index 0000000000..ff99f2e23c --- /dev/null +++ b/test-suite/output/unification.v @@ -0,0 +1,12 @@ +(* Unification error tests *) + +Module A. + +(* Check regression of an UNBOUND_REL bug *) +Inductive T := C : forall {A}, A -> T. +Fail Check fun x => match x return ?[X] with C a => a end. + +(* Bug #3634 *) +Fail Check (id:Type -> _). + +End A. 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/ssr/under.v b/test-suite/ssr/under.v index c12491138a..0312b9c733 100644 --- a/test-suite/ssr/under.v +++ b/test-suite/ssr/under.v @@ -313,8 +313,7 @@ Qed. End TestGeneric2. Section TestPreOrder. -(* inspired by https://github.com/coq/coq/pull/10022#issuecomment-530101950 - but without needing to do [rewrite UnderE] manually. *) +(* inspired by https://github.com/coq/coq/pull/10022#issuecomment-530101950 *) Require Import Morphisms. @@ -330,7 +329,7 @@ Parameter leq_mul : Local Notation "+%N" := addn (at level 0, only parsing). -(** Context lemma (could *) +(** Context lemma *) Lemma leq'_big : forall I (F G : I -> nat) (r : seq I), (forall i : I, leq' (F i) (G i)) -> (leq' (\big[+%N/0%N]_(i <- r) F i) (\big[+%N/0%N]_(i <- r) G i)). @@ -370,8 +369,10 @@ have lem : forall (i : nat), i < n -> leq' (3 + i) (3 + n). under leq'_big => i. { - (* The "magic" is here: instantiate the evar with the bound "3 + n" *) - rewrite lem ?ltn_ord //. over. + rewrite UnderE. + + (* instantiate the evar with the bound "3 + n" *) + apply: lem; exact: ltn_ord. } cbv beta. 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/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/Omega.v b/test-suite/success/Omega.v index 470e4f0580..5e0f90d59b 100644 --- a/test-suite/success/Omega.v +++ b/test-suite/success/Omega.v @@ -90,5 +90,5 @@ Qed. (* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z" *) Lemma lem10 : forall n m:nat, le n (plus n (mult n m)). Proof. -intros; omega with *. +intros; zify; omega. Qed. diff --git a/test-suite/success/OmegaPre.v b/test-suite/success/OmegaPre.v index 17531064cc..0223255067 100644 --- a/test-suite/success/OmegaPre.v +++ b/test-suite/success/OmegaPre.v @@ -16,112 +16,112 @@ Open Scope Z_scope. Goal forall a:Z, Z.max a a = a. intros. -omega with *. +zify; omega. Qed. Goal forall a b:Z, Z.max a b = Z.max b a. intros. -omega with *. +zify; omega. Qed. Goal forall a b c:Z, Z.max a (Z.max b c) = Z.max (Z.max a b) c. intros. -omega with *. +zify; omega. Qed. Goal forall a b:Z, Z.max a b + Z.min a b = a + b. intros. -omega with *. +zify; omega. Qed. Goal forall a:Z, (Z.abs a)*(Z.sgn a) = a. intros. zify. -intuition; subst; omega. (* pure multiplication: omega alone can't do it *) +intuition; subst; zify; omega. (* pure multiplication: zify; omega alone can't do it *) Qed. Goal forall a:Z, Z.abs a = a -> a >= 0. intros. -omega with *. +zify; omega. Qed. Goal forall a:Z, Z.sgn a = a -> a = 1 \/ a = 0 \/ a = -1. intros. -omega with *. +zify; omega. Qed. (* zify_nat *) Goal forall m: nat, (m<2)%nat -> (0<= m+m <=2)%nat. intros. -omega with *. +zify; omega. Qed. Goal forall m:nat, (m<1)%nat -> (m=0)%nat. intros. -omega with *. +zify; omega. Qed. Goal forall m: nat, (m<=100)%nat -> (0<= m+m <=200)%nat. intros. -omega with *. +zify; omega. Qed. (* 2000 instead of 200: works, but quite slow *) Goal forall m: nat, (m*m>=0)%nat. intros. -omega with *. +zify; omega. Qed. (* zify_positive *) Goal forall m: positive, (m<2)%positive -> (2 <= m+m /\ m+m <= 2)%positive. intros. -omega with *. +zify; omega. Qed. Goal forall m:positive, (m<2)%positive -> (m=1)%positive. intros. -omega with *. +zify; omega. Qed. Goal forall m: positive, (m<=1000)%positive -> (2<=m+m/\m+m <=2000)%positive. intros. -omega with *. +zify; omega. Qed. Goal forall m: positive, (m*m>=1)%positive. intros. -omega with *. +zify; omega. Qed. (* zify_N *) Goal forall m:N, (m<2)%N -> (0 <= m+m /\ m+m <= 2)%N. intros. -omega with *. +zify; omega. Qed. Goal forall m:N, (m<1)%N -> (m=0)%N. intros. -omega with *. +zify; omega. Qed. Goal forall m:N, (m<=1000)%N -> (0<=m+m/\m+m <=2000)%N. intros. -omega with *. +zify; omega. Qed. Goal forall m:N, (m*m>=0)%N. intros. -omega with *. +zify; omega. Qed. (* mix of datatypes *) Goal forall p, Z.of_N (N.of_nat (N.to_nat (Npos p))) = Zpos p. intros. -omega with *. +zify; omega. Qed. 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/custom_entry.v b/test-suite/success/custom_entry.v new file mode 100644 index 0000000000..e88ae65e18 --- /dev/null +++ b/test-suite/success/custom_entry.v @@ -0,0 +1,13 @@ +Declare Custom Entry foo. + +Print Custom Grammar foo. + +Notation "[ e ]" := e (e custom foo at level 0). + +Print Custom Grammar foo. + +Notation "1" := O (in custom foo at level 0). + +Print Custom Grammar foo. + +Fail Declare Custom Entry foo. diff --git a/test-suite/success/rapply.v b/test-suite/success/rapply.v new file mode 100644 index 0000000000..13efd986f0 --- /dev/null +++ b/test-suite/success/rapply.v @@ -0,0 +1,27 @@ +Require Import Coq.Program.Tactics. + +(** We make a version of [rapply] that takes [uconstr]; we do not +currently test what scope [rapply] interprets terms in. *) + +Tactic Notation "urapply" uconstr(p) := rapply p. + +Ltac test n := + (*let __ := match goal with _ => idtac n end in*) + lazymatch n with + | O => let __ := match goal with _ => assert True by urapply I; clear end in + uconstr:(fun _ => I) + | S ?n' + => let lem := test n' in + let __ := match goal with _ => assert True by (unshelve urapply lem; try exact I); clear end in + uconstr:(fun _ : True => lem) + end. + +Goal True. + assert True by urapply I. + assert True by (unshelve urapply (fun _ => I); try exact I). + assert True by (unshelve urapply (fun _ _ => I); try exact I). + assert True by (unshelve urapply (fun _ _ _ => I); try exact I). + clear. + Time let __ := test 50 in idtac. + urapply I. +Qed. 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. |