diff options
Diffstat (limited to 'test-suite')
31 files changed, 739 insertions, 16 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index beb80a3dfd..ae426f0daf 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -33,6 +33,7 @@ BIN := $(shell cd ..; pwd)/bin/ coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -batch -test-mode -R prerequisite TestSuite coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite coqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite +coqdoc := $(BIN)coqdoc coqtopbyte := $(BIN)coqtop.byte coqtopload := $(coqtop) -top Top -async-proofs-cache force -load-vernac-source @@ -84,8 +85,11 @@ COMPLEXITY := $(if $(bogomips),complexity) BUGS := bugs/opened bugs/closed +INTERACTIVE := interactive + VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ - output-modulo-time interactive micromega $(COMPLEXITY) modules stm + output-modulo-time $(INTERACTIVE) micromega $(COMPLEXITY) modules stm \ + coqdoc # All subsystems SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coq-makefile @@ -153,6 +157,7 @@ summary: $(call summary_dir, "VI tests", vio); \ $(call summary_dir, "Coqchk tests", coqchk); \ $(call summary_dir, "Coq makefile", coq-makefile); \ + $(call summary_dir, "Coqdoc tests", coqdoc); \ nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \ nb_failure=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_failure) | wc -l`; \ nb_tests=`expr $$nb_success + $$nb_failure`; \ @@ -456,6 +461,8 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake)) fi; \ } > "$@" +# vio compilation + vio: $(patsubst %.v,%.vio.log,$(wildcard vio/*.v)) %.vio.log:%.v @@ -473,6 +480,8 @@ vio: $(patsubst %.v,%.vio.log,$(wildcard vio/*.v)) fi; \ } > "$@" +# coqchk + coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v)) %.chk.log:%.v @@ -489,6 +498,8 @@ coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v)) fi; \ } > "$@" +# coq_makefile + coq-makefile: $(patsubst %/run.sh,%.log,$(wildcard coq-makefile/*/run.sh)) coq-makefile/%.log : coq-makefile/%/run.sh @@ -505,3 +516,27 @@ coq-makefile/%.log : coq-makefile/%/run.sh echo " $<...Error!"; \ fi; \ ) > "$@" + +# coqdoc + +coqdoc: $(patsubst %.sh,%.log,$(wildcard coqdoc/*.sh)) + +$(addsuffix .log,$(wildcard coqdoc/*.v)): %.v.log: %.v %.html.out %.tex.out $(PREREQUISITELOG) + @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" + $(HIDE){ \ + echo $(call log_intro,$<); \ + $(coqc) -R coqdoc Coqdoc $* 2>&1; \ + cd coqdoc; \ + f=`basename $*`; \ + $(coqdoc) -R . Coqdoc -coqlib http://coq.inria.fr/stdlib --html $$f.v; \ + $(coqdoc) -R . Coqdoc -coqlib http://coq.inria.fr/stdlib --latex $$f.v; \ + diff -u --strip-trailing-cr $$f.html.out Coqdoc.$$f.html 2>&1; R=$$?; times; \ + grep -v "^%%" Coqdoc.$$f.tex | diff -u --strip-trailing-cr $$f.tex.out - 2>&1; S=$$?; times; \ + if [ $$R = 0 -a $$S = 0 ]; then \ + echo $(log_success); \ + echo " $<...Ok"; \ + else \ + echo $(log_failure); \ + echo " $<...Error! (unexpected output)"; \ + fi; \ + } > "$@" diff --git a/test-suite/bugs/closed/1859.v b/test-suite/bugs/closed/1859.v new file mode 100644 index 0000000000..43acfe4ba2 --- /dev/null +++ b/test-suite/bugs/closed/1859.v @@ -0,0 +1,20 @@ +Require Import Ring. +Require Import ArithRing. + +Ltac ring_simplify_neq := + match goal with + | [ H: ?X <> ?Y |- _ ] => progress ring_simplify X Y in H + end. + +Lemma toto : forall x y, x*1 <> y*1 -> y*1 <> x*1 -> x<>y. +Proof. + intros. + ring_simplify_neq. + ring_simplify_neq. + (* make sure ring_simplify has simplified both hypotheses *) + match goal with + | [ H: context[_*1] |- _ ] => fail 1 + | _ => idtac + end. + auto. +Qed. diff --git a/test-suite/bugs/closed/5469.v b/test-suite/bugs/closed/5469.v deleted file mode 100644 index fce671c754..0000000000 --- a/test-suite/bugs/closed/5469.v +++ /dev/null @@ -1,3 +0,0 @@ -(* Some problems with the special treatment of curly braces *) - -Reserved Notation "'a' { x }" (at level 0, format "'a' { x }"). diff --git a/test-suite/bugs/closed/5598.v b/test-suite/bugs/closed/5598.v new file mode 100644 index 0000000000..55fef1a575 --- /dev/null +++ b/test-suite/bugs/closed/5598.v @@ -0,0 +1,8 @@ +(* Checking when discharge of an existing class is possible *) +Section foo. + Context {T} (a : T) (b : T). + Let k := eq_refl a. + Existing Class eq. + Fail Global Existing Instance k. + Existing Instance k. +End foo. diff --git a/test-suite/bugs/closed/5608.v b/test-suite/bugs/closed/5608.v new file mode 100644 index 0000000000..f02eae69c2 --- /dev/null +++ b/test-suite/bugs/closed/5608.v @@ -0,0 +1,33 @@ +Reserved Notation "'slet' x .. y := A 'in' b" + (at level 200, x binder, y binder, b at level 200, format "'slet' x .. y := A 'in' '//' b"). +Reserved Notation "T x [1] = { A } ; 'return' ( b0 , b1 , .. , b2 )" + (at level 200, format "T x [1] = { A } ; '//' 'return' ( b0 , b1 , .. , b2 )"). + +Delimit Scope ctype_scope with ctype. +Local Open Scope ctype_scope. +Delimit Scope expr_scope with expr. +Inductive base_type := TZ | TWord (logsz : nat). +Inductive flat_type := Tbase (T : base_type) | Prod (A B : flat_type). +Context {var : base_type -> Type}. +Fixpoint interp_flat_type (interp_base_type : base_type -> Type) (t : +flat_type) := + match t with + | Tbase t => interp_base_type t + | Prod x y => prod (interp_flat_type interp_base_type x) (interp_flat_type +interp_base_type y) + end. +Inductive exprf : flat_type -> Type := +| Var {t} (v : var t) : exprf (Tbase t) +| LetIn {tx} (ex : exprf tx) {tC} (eC : interp_flat_type var tx -> exprf tC) : +exprf tC +| Pair {tx} (ex : exprf tx) {ty} (ey : exprf ty) : exprf (Prod tx ty). +Global Arguments Var {_} _. +Global Arguments LetIn {_} _ {_} _. +Global Arguments Pair {_} _ {_} _. +Notation "T x [1] = { A } ; 'return' ( b0 , b1 , .. , b2 )" := (LetIn (tx:=T) A +(fun x => Pair .. (Pair b0%expr b1%expr) .. b2%expr)) : expr_scope. +Definition foo := + (fun x3 => + (LetIn (Var x3) (fun x18 : var TZ + => (Pair (Var x18) (Var x18))))). +Print foo. diff --git a/test-suite/bugs/closed/HoTT_coq_032.v b/test-suite/bugs/closed/HoTT_coq_032.v index 39a7103d1b..40abb215e9 100644 --- a/test-suite/bugs/closed/HoTT_coq_032.v +++ b/test-suite/bugs/closed/HoTT_coq_032.v @@ -1,4 +1,3 @@ -(* -*- mode: coq; coq-prog-args: ("-xml") -*- *) Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh index 1feff7479b..dc5a500db8 100755 --- a/test-suite/coq-makefile/coqdoc1/run.sh +++ b/test-suite/coq-makefile/coqdoc1/run.sh @@ -15,6 +15,7 @@ sort -u > desired <<EOT ./test ./test/test_plugin.cmi ./test/test_plugin.cmx +./test/test_plugin.cmxa ./test/test_plugin.cmxs ./test/test.glob ./test/test.v diff --git a/test-suite/coq-makefile/coqdoc2/run.sh b/test-suite/coq-makefile/coqdoc2/run.sh index 1feff7479b..dc5a500db8 100755 --- a/test-suite/coq-makefile/coqdoc2/run.sh +++ b/test-suite/coq-makefile/coqdoc2/run.sh @@ -15,6 +15,7 @@ sort -u > desired <<EOT ./test ./test/test_plugin.cmi ./test/test_plugin.cmx +./test/test_plugin.cmxa ./test/test_plugin.cmxs ./test/test.glob ./test/test.v diff --git a/test-suite/coq-makefile/findlib-package/Makefile.local b/test-suite/coq-makefile/findlib-package/Makefile.local new file mode 100644 index 0000000000..0f4a7d9954 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package/Makefile.local @@ -0,0 +1 @@ +CAMLPKGS += -package foo diff --git a/test-suite/coq-makefile/findlib-package/_CoqProject b/test-suite/coq-makefile/findlib-package/_CoqProject new file mode 100644 index 0000000000..69f47302e1 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package/_CoqProject @@ -0,0 +1,10 @@ +-R src test +-R theories test +-I src + +src/test_plugin.mlpack +src/test.ml4 +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v diff --git a/test-suite/coq-makefile/findlib-package/findlib/foo/META b/test-suite/coq-makefile/findlib-package/findlib/foo/META new file mode 100644 index 0000000000..ff5f1c7c96 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package/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/findlib/foo/Makefile b/test-suite/coq-makefile/findlib-package/findlib/foo/Makefile new file mode 100644 index 0000000000..31cf116652 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package/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/findlib/foo/foo.mli b/test-suite/coq-makefile/findlib-package/findlib/foo/foo.mli new file mode 100644 index 0000000000..e69de29bb2 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package/findlib/foo/foo.mli diff --git a/test-suite/coq-makefile/findlib-package/findlib/foo/foolib.ml b/test-suite/coq-makefile/findlib-package/findlib/foo/foolib.ml new file mode 100644 index 0000000000..81306fb89b --- /dev/null +++ b/test-suite/coq-makefile/findlib-package/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/run.sh b/test-suite/coq-makefile/findlib-package/run.sh new file mode 100755 index 0000000000..a0d8a7fea7 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package/run.sh @@ -0,0 +1,13 @@ +#!/usr/bin/env bash + +. ../template/init.sh + +echo "let () = Foolib.foo ();;" >> src/test_aux.ml +export OCAMLPATH=$OCAMLPATH:$PWD/findlib +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/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh index 51669f28f5..03df9cf050 100755 --- a/test-suite/coq-makefile/mlpack1/run.sh +++ b/test-suite/coq-makefile/mlpack1/run.sh @@ -15,6 +15,7 @@ sort > desired <<EOT ./test/test.glob ./test/test_plugin.cmi ./test/test_plugin.cmx +./test/test_plugin.cmxa ./test/test_plugin.cmxs ./test/test.v ./test/test.vo diff --git a/test-suite/coq-makefile/mlpack2/run.sh b/test-suite/coq-makefile/mlpack2/run.sh index 51669f28f5..03df9cf050 100755 --- a/test-suite/coq-makefile/mlpack2/run.sh +++ b/test-suite/coq-makefile/mlpack2/run.sh @@ -15,6 +15,7 @@ sort > desired <<EOT ./test/test.glob ./test/test_plugin.cmi ./test/test_plugin.cmx +./test/test_plugin.cmxa ./test/test_plugin.cmxs ./test/test.v ./test/test.vo diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh index 3bec11cb75..89bafe9ad1 100755 --- a/test-suite/coq-makefile/native1/run.sh +++ b/test-suite/coq-makefile/native1/run.sh @@ -18,6 +18,7 @@ sort > desired <<EOT ./test/test.glob ./test/test_plugin.cmi ./test/test_plugin.cmx +./test/test_plugin.cmxa ./test/test_plugin.cmxs ./test/test.v ./test/test.vo diff --git a/test-suite/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v index a978f6b901..7906a5b15e 100644 --- a/test-suite/coqchk/cumulativity.v +++ b/test-suite/coqchk/cumulativity.v @@ -1,5 +1,5 @@ Set Universe Polymorphism. -Set Inductive Cumulativity. +Set Polymorphic Inductive Cumulativity. Set Printing Universes. Inductive List (A: Type) := nil | cons : A -> List A -> List A. diff --git a/test-suite/coqdoc/bug5648.html.out b/test-suite/coqdoc/bug5648.html.out new file mode 100644 index 0000000000..06789c1c10 --- /dev/null +++ b/test-suite/coqdoc/bug5648.html.out @@ -0,0 +1,53 @@ +<!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=iso-8859-1" /> +<link href="coqdoc.css" rel="stylesheet" type="text/css" /> +<title>Coqdoc.bug5648</title> +</head> + +<body> + +<div id="page"> + +<div id="header"> +</div> + +<div id="main"> + +<h1 class="libtitle">Library Coqdoc.bug5648</h1> + +<div class="code"> +<span class="id" title="keyword">Lemma</span> <a name="a"><span class="id" title="lemma">a</span></a> : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a>.<br/> +<span class="id" title="keyword">Proof</span>.<br/> +<span class="id" title="tactic">auto</span>.<br/> +<span class="id" title="keyword">Qed</span>.<br/> + +<br/> +<span class="id" title="keyword">Variant</span> <a name="t"><span class="id" title="inductive">t</span></a> :=<br/> +| <a name="A"><span class="id" title="constructor">A</span></a> | <a name="Add"><span class="id" title="constructor">Add</span></a> | <a name="G"><span class="id" title="constructor">G</span></a> | <a name="Goal"><span class="id" title="constructor">Goal</span></a> | <a name="L"><span class="id" title="constructor">L</span></a> | <a name="Lemma"><span class="id" title="constructor">Lemma</span></a> | <a name="P"><span class="id" title="constructor">P</span></a> | <a name="Proof"><span class="id" title="constructor">Proof</span></a> .<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="d"><span class="id" title="definition">d</span></a> <span class="id" title="var">x</span> :=<br/> + <span class="id" title="keyword">match</span> <a class="idref" href="Coqdoc.bug5648.html#x"><span class="id" title="variable">x</span></a> <span class="id" title="keyword">with</span><br/> + | <a class="idref" href="Coqdoc.bug5648.html#A"><span class="id" title="constructor">A</span></a> => 0<br/> + | <a class="idref" href="Coqdoc.bug5648.html#Add"><span class="id" title="constructor">Add</span></a> => 1<br/> + | <a class="idref" href="Coqdoc.bug5648.html#G"><span class="id" title="constructor">G</span></a> => 2<br/> + | <a class="idref" href="Coqdoc.bug5648.html#Goal"><span class="id" title="constructor">Goal</span></a> => 3<br/> + | <a class="idref" href="Coqdoc.bug5648.html#L"><span class="id" title="constructor">L</span></a> => 4<br/> + | <a class="idref" href="Coqdoc.bug5648.html#Lemma"><span class="id" title="constructor">Lemma</span></a> => 5<br/> + | <a class="idref" href="Coqdoc.bug5648.html#P"><span class="id" title="constructor">P</span></a> => 6<br/> + | <a class="idref" href="Coqdoc.bug5648.html#Proof"><span class="id" title="constructor">Proof</span></a> => 7<br/> + <span class="id" title="keyword">end</span>.<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/bug5648.tex.out b/test-suite/coqdoc/bug5648.tex.out new file mode 100644 index 0000000000..b0b732effa --- /dev/null +++ b/test-suite/coqdoc/bug5648.tex.out @@ -0,0 +1,49 @@ +\documentclass[12pt]{report} +\usepackage[]{inputenc} +\usepackage[T1]{fontenc} +\usepackage{fullpage} +\usepackage{coqdoc} +\usepackage{amsmath,amssymb} +\usepackage{url} +\begin{document} +\coqlibrary{Coqdoc.bug5648}{Library }{Coqdoc.bug5648} + +\begin{coqdoccode} +\coqdocnoindent +\coqdockw{Lemma} \coqdef{Coqdoc.bug5648.a}{a}{\coqdoclemma{a}} : \coqexternalref{True}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocinductive{True}}.\coqdoceol +\coqdocnoindent +\coqdockw{Proof}.\coqdoceol +\coqdocnoindent +\coqdoctac{auto}.\coqdoceol +\coqdocnoindent +\coqdockw{Qed}.\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdockw{Variant} \coqdef{Coqdoc.bug5648.t}{t}{\coqdocinductive{t}} :=\coqdoceol +\coqdocnoindent +\ensuremath{|} \coqdef{Coqdoc.bug5648.A}{A}{\coqdocconstructor{A}} \ensuremath{|} \coqdef{Coqdoc.bug5648.Add}{Add}{\coqdocconstructor{Add}} \ensuremath{|} \coqdef{Coqdoc.bug5648.G}{G}{\coqdocconstructor{G}} \ensuremath{|} \coqdef{Coqdoc.bug5648.Goal}{Goal}{\coqdocconstructor{Goal}} \ensuremath{|} \coqdef{Coqdoc.bug5648.L}{L}{\coqdocconstructor{L}} \ensuremath{|} \coqdef{Coqdoc.bug5648.Lemma}{Lemma}{\coqdocconstructor{Lemma}} \ensuremath{|} \coqdef{Coqdoc.bug5648.P}{P}{\coqdocconstructor{P}} \ensuremath{|} \coqdef{Coqdoc.bug5648.Proof}{Proof}{\coqdocconstructor{Proof}} .\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdockw{Definition} \coqdef{Coqdoc.bug5648.d}{d}{\coqdocdefinition{d}} \coqdocvar{x} :=\coqdoceol +\coqdocindent{1.00em} +\coqdockw{match} \coqdocvariable{x} \coqdockw{with}\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqref{Coqdoc.bug5648.A}{\coqdocconstructor{A}} \ensuremath{\Rightarrow} 0\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqref{Coqdoc.bug5648.Add}{\coqdocconstructor{Add}} \ensuremath{\Rightarrow} 1\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqref{Coqdoc.bug5648.G}{\coqdocconstructor{G}} \ensuremath{\Rightarrow} 2\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqref{Coqdoc.bug5648.Goal}{\coqdocconstructor{Goal}} \ensuremath{\Rightarrow} 3\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqref{Coqdoc.bug5648.L}{\coqdocconstructor{L}} \ensuremath{\Rightarrow} 4\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqref{Coqdoc.bug5648.Lemma}{\coqdocconstructor{Lemma}} \ensuremath{\Rightarrow} 5\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqref{Coqdoc.bug5648.P}{\coqdocconstructor{P}} \ensuremath{\Rightarrow} 6\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqref{Coqdoc.bug5648.Proof}{\coqdocconstructor{Proof}} \ensuremath{\Rightarrow} 7\coqdoceol +\coqdocindent{1.00em} +\coqdockw{end}.\coqdoceol +\end{coqdoccode} +\end{document} diff --git a/test-suite/coqdoc/bug5648.v b/test-suite/coqdoc/bug5648.v new file mode 100644 index 0000000000..9b62dd1e1e --- /dev/null +++ b/test-suite/coqdoc/bug5648.v @@ -0,0 +1,19 @@ +Lemma a : True. +Proof. +auto. +Qed. + +Variant t := +| A | Add | G | Goal | L | Lemma | P | Proof . + +Definition d x := + match x with + | A => 0 + | Add => 1 + | G => 2 + | Goal => 3 + | L => 4 + | Lemma => 5 + | P => 6 + | Proof => 7 + end. diff --git a/test-suite/coqdoc/links.html.out b/test-suite/coqdoc/links.html.out new file mode 100644 index 0000000000..7d7d01c1b4 --- /dev/null +++ b/test-suite/coqdoc/links.html.out @@ -0,0 +1,206 @@ +<!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=iso-8859-1" /> +<link href="coqdoc.css" rel="stylesheet" type="text/css" /> +<title>Coqdoc.links</title> +</head> + +<body> + +<div id="page"> + +<div id="header"> +</div> + +<div id="main"> + +<h1 class="libtitle">Library Coqdoc.links</h1> + +<div class="code"> +</div> + +<div class="doc"> +Various checks for coqdoc + +<div class="paragraph"> </div> + +<ul class="doclist"> +<li> symbols should not be inlined in string g + +</li> +<li> links to both kinds of notations in a' should work to the right notation + +</li> +<li> with utf8 option, forall must be unicode + +</li> +<li> splitting between symbols and ident should be correct in a' and c + +</li> +<li> ".." should be rendered correctly + +</li> +</ul> + +</div> +<div class="code"> + +<br/> +<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Strings.String.html#"><span class="id" title="library">String</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="g"><span class="id" title="definition">g</span></a> := "dfjkh""sdfhj forall <> * ~"%<span class="id" title="var">string</span>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="a"><span class="id" title="definition">a</span></a> (<span class="id" title="var">b</span>: <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) := <a class="idref" href="Coqdoc.links.html#b"><span class="id" title="variable">b</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="f"><span class="id" title="definition">f</span></a> := <span class="id" title="keyword">forall</span> <span class="id" title="var">C</span>:<span class="id" title="keyword">Prop</span>, <a class="idref" href="Coqdoc.links.html#C"><span class="id" title="variable">C</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="1a1c7f13320341c3638e9edcc3e6389d"><span class="id" title="notation">"</span></a>n ++ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>).<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="1a1c7f13320341c3638e9edcc3e6389d"><span class="id" title="notation">"</span></a>n ++ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#mult"><span class="id" title="abbreviation">mult</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>). +<br/> +<span class="id" title="keyword">Notation</span> <a name="6b97e27793a3d22f5c0d1dd63170fd68"><span class="id" title="notation">"</span></a>n ** m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 60).<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="3e01fbae4590c7b7699ff99ce61580e1"><span class="id" title="notation">"</span></a>n ▵ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 60).<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">"</span></a>n '_' ++ 'x' m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 3).<br/> + +<br/> +<span class="id" title="keyword">Inductive</span> <a name="eq"><span class="id" title="inductive">eq</span></a> (<span class="id" title="var">A</span>:<span class="id" title="keyword">Type</span>) (<span class="id" title="var">x</span>:<a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a>) : <span class="id" title="var">A</span> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">-></span></a> <span class="id" title="keyword">Prop</span> := <a name="eq_refl"><span class="id" title="constructor">eq_refl</span></a> : <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:></span></a><a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a><br/> +<br/> +<span class="id" title="keyword">where</span> <a name="8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">"</span></a>x = y :> A" := (@<a class="idref" href="Coqdoc.links.html#eq"><span class="id" title="variable">eq</span></a> <span class="id" title="var">A</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) : <span class="id" title="var">type_scope</span>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="eq0"><span class="id" title="definition">eq0</span></a> := 0 <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:></span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="548d1059c499c9b2a9b95b07e68c2090"><span class="id" title="notation">"</span></a>( x # y ; .. ; z )" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#pair"><span class="id" title="constructor">pair</span></a> .. (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#pair"><span class="id" title="constructor">pair</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) .. <span class="id" title="var">z</span>).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="9f5a1d89cbd4d38f5e289576db7123d1"><span class="id" title="definition">b_α</span></a> := <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="Coqdoc.links.html#548d1059c499c9b2a9b95b07e68c2090"><span class="id" title="notation">(</span></a>0<a class="idref" href="Coqdoc.links.html#548d1059c499c9b2a9b95b07e68c2090"><span class="id" title="notation">#</span></a>0<a class="idref" href="Coqdoc.links.html#548d1059c499c9b2a9b95b07e68c2090"><span class="id" title="notation">;</span></a>0<a class="idref" href="Coqdoc.links.html#548d1059c499c9b2a9b95b07e68c2090"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a>0 <a class="idref" href="Coqdoc.links.html#6b97e27793a3d22f5c0d1dd63170fd68"><span class="id" title="notation">**</span></a> 0<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">))</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="h"><span class="id" title="abbreviation">h</span></a> := <a class="idref" href="Coqdoc.links.html#a"><span class="id" title="definition">a</span></a>.<br/> + +<br/> + <span class="id" title="keyword">Section</span> <a name="test"><span class="id" title="section">test</span></a>.<br/> + +<br/> + <span class="id" title="keyword">Variables</span> <a name="test.b'"><span class="id" title="variable">b'</span></a> <a name="test.b2"><span class="id" title="variable">b2</span></a>: <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> + +<br/> + <span class="id" title="keyword">Notation</span> <a name="4ab0449b36c75cf94e08c5822ea83e3d"><span class="id" title="notation">"</span></a>n + m" := (<span class="id" title="var">n</span> <a class="idref" href="Coqdoc.links.html#3e01fbae4590c7b7699ff99ce61580e1"><span class="id" title="notation">▵</span></a> <span class="id" title="var">m</span>) : <span class="id" title="var">my_scope</span>.<br/> + +<br/> + <span class="id" title="keyword">Delimit</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">my_scope</span> <span class="id" title="keyword">with</span> <span class="id" title="var">my</span>.<br/> + +<br/> + <span class="id" title="keyword">Notation</span> <a name="l"><span class="id" title="abbreviation">l</span></a> := 0.<br/> + +<br/> + <span class="id" title="keyword">Definition</span> <a name="ab410a966ac148e9b78c65c6cdf301fd"><span class="id" title="definition">α</span></a> := (0 <a class="idref" href="Coqdoc.links.html#4ab0449b36c75cf94e08c5822ea83e3d"><span class="id" title="notation">+</span></a> <a class="idref" href="Coqdoc.links.html#l"><span class="id" title="abbreviation">l</span></a>)%<span class="id" title="var">my</span>.<br/> + +<br/> + <span class="id" title="keyword">Definition</span> <a name="a'"><span class="id" title="definition">a'</span></a> <span class="id" title="var">b</span> := <a class="idref" href="Coqdoc.links.html#test.b'"><span class="id" title="variable">b'</span></a><a class="idref" href="Coqdoc.links.html#1a1c7f13320341c3638e9edcc3e6389d"><span class="id" title="notation">++</span></a>0<a class="idref" href="Coqdoc.links.html#1a1c7f13320341c3638e9edcc3e6389d"><span class="id" title="notation">++</span></a><a class="idref" href="Coqdoc.links.html#test.b2"><span class="id" title="variable">b2</span></a> <a class="idref" href="Coqdoc.links.html#347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">_</span></a> <a class="idref" href="Coqdoc.links.html#347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">++</span></a><a class="idref" href="Coqdoc.links.html#347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">x</span></a> <a class="idref" href="Coqdoc.links.html#b"><span class="id" title="variable">b</span></a>.<br/> + +<br/> + <span class="id" title="keyword">Definition</span> <a name="c"><span class="id" title="definition">c</span></a> := <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Specif.html#5bf2050e90b21ebc82dc5463d1ba338e"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Specif.html#5bf2050e90b21ebc82dc5463d1ba338e"><span class="id" title="notation">}+{</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Specif.html#5bf2050e90b21ebc82dc5463d1ba338e"><span class="id" title="notation">}</span></a>.<br/> + +<br/> + <span class="id" title="keyword">Definition</span> <a name="d"><span class="id" title="definition">d</span></a> := (1<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#b3eea360671e1b32b18a26e15b3aace3"><span class="id" title="notation">+</span></a>2)%<span class="id" title="var">nat</span>.<br/> + +<br/> + <span class="id" title="keyword">Lemma</span> <a name="e"><span class="id" title="lemma">e</span></a> : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#3dcaec3b772747610227247939f96b01"><span class="id" title="notation">+</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> + <span class="id" title="var">Admitted</span>.<br/> + +<br/> + <span class="id" title="keyword">End</span> <a class="idref" href="Coqdoc.links.html#test"><span class="id" title="section">test</span></a>.<br/> + +<br/> + <span class="id" title="keyword">Section</span> <a name="test2"><span class="id" title="section">test2</span></a>.<br/> + +<br/> + <span class="id" title="keyword">Variables</span> <a name="test2.b'"><span class="id" title="variable">b'</span></a>: <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> + +<br/> + <span class="id" title="keyword">Section</span> <a name="test2.test"><span class="id" title="section">test</span></a>.<br/> + +<br/> + <span class="id" title="keyword">Variables</span> <a name="test2.test.b2"><span class="id" title="variable">b2</span></a>: <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> + +<br/> + <span class="id" title="keyword">Definition</span> <a name="a''"><span class="id" title="definition">a''</span></a> <span class="id" title="var">b</span> := <a class="idref" href="Coqdoc.links.html#test2.b'"><span class="id" title="variable">b'</span></a> <a class="idref" href="Coqdoc.links.html#1a1c7f13320341c3638e9edcc3e6389d"><span class="id" title="notation">++</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#O"><span class="id" title="constructor">O</span></a> <a class="idref" href="Coqdoc.links.html#1a1c7f13320341c3638e9edcc3e6389d"><span class="id" title="notation">++</span></a> <a class="idref" href="Coqdoc.links.html#test2.test.b2"><span class="id" title="variable">b2</span></a> <a class="idref" href="Coqdoc.links.html#347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">_</span></a> <a class="idref" href="Coqdoc.links.html#347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">++</span></a> <a class="idref" href="Coqdoc.links.html#347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">x</span></a> <a class="idref" href="Coqdoc.links.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#b3eea360671e1b32b18a26e15b3aace3"><span class="id" title="notation">+</span></a> <a class="idref" href="Coqdoc.links.html#h"><span class="id" title="abbreviation">h</span></a> 0.<br/> + +<br/> + <span class="id" title="keyword">End</span> <a class="idref" href="Coqdoc.links.html#test2.test"><span class="id" title="section">test</span></a>.<br/> + +<br/> + <span class="id" title="keyword">End</span> <a class="idref" href="Coqdoc.links.html#test2"><span class="id" title="section">test2</span></a>.<br/> + +<br/> +</div> + +<div class="doc"> +skip +<div class="paragraph"> </div> + + skip +<div class="paragraph"> </div> + + skip +<div class="paragraph"> </div> + + skip +<div class="paragraph"> </div> + + skip +<div class="paragraph"> </div> + + skip +<div class="paragraph"> </div> + + skip +<div class="paragraph"> </div> + + skip +<div class="paragraph"> </div> + + skip +<div class="paragraph"> </div> + + skip +<div class="paragraph"> </div> + + skip +<div class="paragraph"> </div> + + skip +<div class="paragraph"> </div> + + skip +<div class="paragraph"> </div> + + skip +</div> +<div class="code"> + +<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/links.tex.out b/test-suite/coqdoc/links.tex.out new file mode 100644 index 0000000000..844fb3031c --- /dev/null +++ b/test-suite/coqdoc/links.tex.out @@ -0,0 +1,162 @@ +\documentclass[12pt]{report} +\usepackage[]{inputenc} +\usepackage[T1]{fontenc} +\usepackage{fullpage} +\usepackage{coqdoc} +\usepackage{amsmath,amssymb} +\usepackage{url} +\begin{document} +\coqlibrary{Coqdoc.links}{Library }{Coqdoc.links} + +\begin{coqdoccode} +\end{coqdoccode} +Various checks for coqdoc + + + +\begin{itemize} +\item symbols should not be inlined in string g + +\item links to both kinds of notations in a' should work to the right notation + +\item with utf8 option, forall must be unicode + +\item splitting between symbols and ident should be correct in a' and c + +\item ``..'' should be rendered correctly + +\end{itemize} +\begin{coqdoccode} +\coqdocemptyline +\coqdocnoindent +\coqdockw{Require} \coqdockw{Import} \coqexternalref{}{http://coq.inria.fr/stdlib/Coq.Strings.String}{\coqdoclibrary{String}}.\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdockw{Definition} \coqdef{Coqdoc.links.g}{g}{\coqdocdefinition{g}} := "dfjkh""sdfhj forall <> * \~{}"\%\coqdocvar{string}.\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdockw{Definition} \coqdef{Coqdoc.links.a}{a}{\coqdocdefinition{a}} (\coqdocvar{b}: \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}) := \coqdocvariable{b}.\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdockw{Definition} \coqdef{Coqdoc.links.f}{f}{\coqdocdefinition{f}} := \coqdockw{\ensuremath{\forall}} \coqdocvar{C}:\coqdockw{Prop}, \coqdocvariable{C}.\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdockw{Notation} \coqdef{Coqdoc.links.::x '++' x}{"}{"}n ++ m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}).\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdockw{Notation} \coqdef{Coqdoc.links.::x '++' x}{"}{"}n ++ m" := (\coqexternalref{mult}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{mult}} \coqdocvar{n} \coqdocvar{m}). \coqdocemptyline +\coqdocnoindent +\coqdockw{Notation} \coqdef{Coqdoc.links.::x '**' x}{"}{"}n ** m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}) (\coqdoctac{at} \coqdockw{level} 60).\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdockw{Notation} \coqdef{Coqdoc.links.::x 'xE2x96xB5' x}{"}{"}n ▵ m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}) (\coqdoctac{at} \coqdockw{level} 60).\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdockw{Notation} \coqdef{Coqdoc.links.::x ''' ''' '++' 'x' x}{"}{"}n '\_' ++ 'x' m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}) (\coqdoctac{at} \coqdockw{level} 3).\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdockw{Inductive} \coqdef{Coqdoc.links.eq}{eq}{\coqdocinductive{eq}} (\coqdocvar{A}:\coqdockw{Type}) (\coqdocvar{x}:\coqdocvariable{A}) : \coqdocvar{A} \coqexternalref{:type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqdockw{Prop} := \coqdef{Coqdoc.links.eq refl}{eq\_refl}{\coqdocconstructor{eq\_refl}} : \coqdocvariable{x} \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{=}} \coqdocvariable{x} \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{:>}}\coqdocvariable{A}\coqdoceol +\coqdocnoindent +\coqdoceol +\coqdocnoindent +\coqdockw{where} \coqdef{Coqdoc.links.:type scope:x '=' x ':>' x}{"}{"}x = y :> A" := (@\coqdocvariable{eq} \coqdocvar{A} \coqdocvar{x} \coqdocvar{y}) : \coqdocvar{type\_scope}.\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdockw{Definition} \coqdef{Coqdoc.links.eq0}{eq0}{\coqdocdefinition{eq0}} := 0 \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{=}} 0 \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{:>}} \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdockw{Notation} \coqdef{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{"}{"}( x \# y ; .. ; z )" := (\coqexternalref{pair}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{pair}} .. (\coqexternalref{pair}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{pair}} \coqdocvar{x} \coqdocvar{y}) .. \coqdocvar{z}).\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdockw{Definition} \coqdef{Coqdoc.links.b xCExB1}{b\_α}{\coqdocdefinition{b\_α}} := \coqexternalref{:core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{(}}\coqref{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{(}}0\coqref{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{\#}}0\coqref{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{;}}0\coqref{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{)}} \coqexternalref{:core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{,}} \coqexternalref{:core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{(}}0 \coqref{Coqdoc.links.::x '**' x}{\coqdocnotation{**}} 0\coqexternalref{:core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{))}}.\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdockw{Notation} \coqdef{Coqdoc.links.h}{h}{\coqdocabbreviation{h}} := \coqref{Coqdoc.links.a}{\coqdocdefinition{a}}.\coqdoceol +\coqdocemptyline +\coqdocindent{1.00em} +\coqdockw{Section} \coqdef{Coqdoc.links.test}{test}{\coqdocsection{test}}.\coqdoceol +\coqdocemptyline +\coqdocindent{2.00em} +\coqdockw{Variables} \coqdef{Coqdoc.links.test.b'}{b'}{\coqdocvariable{b'}} \coqdef{Coqdoc.links.test.b2}{b2}{\coqdocvariable{b2}}: \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol +\coqdocemptyline +\coqdocindent{2.00em} +\coqdockw{Notation} \coqdef{Coqdoc.links.test.:my scope:x '+' x}{"}{"}n + m" := (\coqdocvar{n} \coqref{Coqdoc.links.::x 'xE2x96xB5' x}{\coqdocnotation{▵}} \coqdocvar{m}) : \coqdocvar{my\_scope}.\coqdoceol +\coqdocemptyline +\coqdocindent{2.00em} +\coqdockw{Delimit} \coqdockw{Scope} \coqdocvar{my\_scope} \coqdockw{with} \coqdocvar{my}.\coqdoceol +\coqdocemptyline +\coqdocindent{2.00em} +\coqdockw{Notation} \coqdef{Coqdoc.links.l}{l}{\coqdocabbreviation{l}} := 0.\coqdoceol +\coqdocemptyline +\coqdocindent{2.00em} +\coqdockw{Definition} \coqdef{Coqdoc.links.xCExB1}{α}{\coqdocdefinition{α}} := (0 \coqref{Coqdoc.links.test.:my scope:x '+' x}{\coqdocnotation{+}} \coqref{Coqdoc.links.l}{\coqdocabbreviation{l}})\%\coqdocvar{my}.\coqdoceol +\coqdocemptyline +\coqdocindent{2.00em} +\coqdockw{Definition} \coqdef{Coqdoc.links.a'}{a'}{\coqdocdefinition{a'}} \coqdocvar{b} := \coqdocvariable{b'}\coqref{Coqdoc.links.::x '++' x}{\coqdocnotation{++}}0\coqref{Coqdoc.links.::x '++' x}{\coqdocnotation{++}}\coqdocvariable{b2} \coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{\_}} \coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{++}}\coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{x}} \coqdocvariable{b}.\coqdoceol +\coqdocemptyline +\coqdocindent{2.00em} +\coqdockw{Definition} \coqdef{Coqdoc.links.c}{c}{\coqdocdefinition{c}} := \coqexternalref{:type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\{}}\coqexternalref{True}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocinductive{True}}\coqexternalref{:type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\}+\{}}\coqexternalref{True}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocinductive{True}}\coqexternalref{:type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\}}}.\coqdoceol +\coqdocemptyline +\coqdocindent{2.00em} +\coqdockw{Definition} \coqdef{Coqdoc.links.d}{d}{\coqdocdefinition{d}} := (1\coqexternalref{:nat scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocnotation{+}}2)\%\coqdocvar{nat}.\coqdoceol +\coqdocemptyline +\coqdocindent{2.00em} +\coqdockw{Lemma} \coqdef{Coqdoc.links.e}{e}{\coqdoclemma{e}} : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}} \coqexternalref{:type scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{+}} \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol +\coqdocindent{2.00em} +\coqdocvar{Admitted}.\coqdoceol +\coqdocemptyline +\coqdocindent{1.00em} +\coqdockw{End} \coqref{Coqdoc.links.test}{\coqdocsection{test}}.\coqdoceol +\coqdocemptyline +\coqdocindent{1.00em} +\coqdockw{Section} \coqdef{Coqdoc.links.test2}{test2}{\coqdocsection{test2}}.\coqdoceol +\coqdocemptyline +\coqdocindent{2.00em} +\coqdockw{Variables} \coqdef{Coqdoc.links.test2.b'}{b'}{\coqdocvariable{b'}}: \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol +\coqdocemptyline +\coqdocindent{2.00em} +\coqdockw{Section} \coqdef{Coqdoc.links.test2.test}{test}{\coqdocsection{test}}.\coqdoceol +\coqdocemptyline +\coqdocindent{3.00em} +\coqdockw{Variables} \coqdef{Coqdoc.links.test2.test.b2}{b2}{\coqdocvariable{b2}}: \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol +\coqdocemptyline +\coqdocindent{3.00em} +\coqdockw{Definition} \coqdef{Coqdoc.links.a''}{a'{}'}{\coqdocdefinition{a'{}'}} \coqdocvar{b} := \coqdocvariable{b'} \coqref{Coqdoc.links.::x '++' x}{\coqdocnotation{++}} \coqexternalref{O}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{O}} \coqref{Coqdoc.links.::x '++' x}{\coqdocnotation{++}} \coqdocvariable{b2} \coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{\_}} \coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{++}} \coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{x}} \coqdocvariable{b} \coqexternalref{:nat scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocnotation{+}} \coqref{Coqdoc.links.h}{\coqdocabbreviation{h}} 0.\coqdoceol +\coqdocemptyline +\coqdocindent{2.00em} +\coqdockw{End} \coqref{Coqdoc.links.test2.test}{\coqdocsection{test}}.\coqdoceol +\coqdocemptyline +\coqdocindent{1.00em} +\coqdockw{End} \coqref{Coqdoc.links.test2}{\coqdocsection{test2}}.\coqdoceol +\coqdocemptyline +\end{coqdoccode} +skip + + skip + + skip + + skip + + skip + + skip + + skip + + skip + + skip + + skip + + skip + + skip + + skip + + skip \begin{coqdoccode} +\coqdocemptyline +\end{coqdoccode} +\end{document} diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index a9ae74fd67..e5dbfcb4be 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -1,3 +1,5 @@ +{x : nat | x = 0} + {True /\ False} + {forall x : nat, x = 0} + : Set [<0, 2 >] : nat * nat * (nat * nat) [<0, 2 >] @@ -109,9 +111,14 @@ fun x : ?A => x === x : forall x : ?A, x = x where ?A : [x : ?A |- Type] (x cannot be used) -{0, 1} +{{0, 1}} : nat * nat -{0, 1, 2} +{{0, 1, 2}} : nat * (nat * nat) -{0, 1, 2, 3} +{{0, 1, 2, 3}} : nat * (nat * (nat * nat)) +letpair x [1] = {0}; +return (1, 2, 3, 4) + : nat * nat * nat * nat +{{ 1 | 1 // 1 }} + : nat diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index dee0f70f79..b1015137d6 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -1,4 +1,9 @@ (**********************************************************************) +(* Check precedence, spacing, etc. in printing with curly brackets *) + +Check {x|x=0}+{True/\False}+{forall x, x=0}. + +(**********************************************************************) (* Check printing of notations with several instances of a recursive pattern *) (* Was wrong but I could not trigger a problem due to the collision between *) (* different instances of ".." *) @@ -161,10 +166,23 @@ End Bug4765. Notation "x === x" := (eq_refl x) (only printing, at level 10). Check (fun x => eq_refl x). -(**********************************************************************) (* Test recursive notations with the recursive pattern repeated on the right *) -Notation "{ x , .. , y , z }" := (pair x .. (pair y z) ..). -Check {0,1}. -Check {0,1,2}. -Check {0,1,2,3}. +Notation "{{ x , .. , y , z }}" := (pair x .. (pair y z) ..). +Check {{0,1}}. +Check {{0,1,2}}. +Check {{0,1,2,3}}. + +(* Test printing of #5608 *) + +Reserved Notation "'letpair' x [1] = { A } ; 'return' ( b0 , b1 , .. , b2 )" + (at level 200, format "'letpair' x [1] = { A } ; '//' 'return' ( b0 , b1 , .. , b2 )"). +Notation "'letpair' x [1] = { a } ; 'return' ( b0 , b1 , .. , b2 )" := + (let x:=a in ( .. (b0,b1) .., b2)). +Check letpair x [1] = {0}; return (1,2,3,4). + +(* Test spacing in #5569 *) + +Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut) + (at level 0, xR at level 39, format "{ { xL | xR // xcut } }"). +Check 1+1+1. diff --git a/test-suite/output/UnclosedBlocks.out b/test-suite/output/UnclosedBlocks.out new file mode 100644 index 0000000000..b83e94ad43 --- /dev/null +++ b/test-suite/output/UnclosedBlocks.out @@ -0,0 +1,3 @@ + +Error: The section Baz, module type Bar and module Foo need to be closed. + diff --git a/test-suite/output/UnclosedBlocks.v b/test-suite/output/UnclosedBlocks.v new file mode 100644 index 0000000000..854bd6a6d5 --- /dev/null +++ b/test-suite/output/UnclosedBlocks.v @@ -0,0 +1,8 @@ +(* -*- mode: coq; coq-prog-args: ("-compile" "UnclosedBlocks.v") *) +Module Foo. + Module Closed. + End Closed. + Module Type Bar. + Section Baz. + (* end-of-compilation error message reports unclosed sections, blocks, and + module types *) diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v index ebf817cfc5..0ee85712e2 100644 --- a/test-suite/success/cumulativity.v +++ b/test-suite/success/cumulativity.v @@ -1,5 +1,11 @@ +Polymorphic Cumulative Inductive T1 := t1 : T1. +Fail Monomorphic Cumulative Inductive T2 := t2 : T2. + +Polymorphic Cumulative Record R1 := { r1 : T1 }. +Fail Monomorphic Cumulative Inductive R2 := {r2 : T1}. + Set Universe Polymorphism. -Set Inductive Cumulativity. +Set Polymorphic Inductive Cumulativity. Set Printing Universes. Inductive List (A: Type) := nil | cons : A -> List A -> List A. @@ -62,4 +68,33 @@ End subtyping_test. Record A : Type := { a :> Type; }. -Record B (X : A) : Type := { b : X; }.
\ No newline at end of file +Record B (X : A) : Type := { b : X; }. + +NonCumulative Inductive NCList (A: Type) + := ncnil | nccons : A -> NCList A -> NCList A. + +Section NCListLift. + Universe i j. + + Constraint i < j. + + Fail Definition LiftNCL {A} : NCList@{i} A -> NCList@{j} A := fun x => x. + +End NCListLift. + +Inductive eq@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := eq_refl : eq x x. + +Definition funext_type@{a b e} (A : Type@{a}) (B : A -> Type@{b}) + := forall f g : (forall a, B a), + (forall x, eq@{e} (f x) (g x)) + -> eq@{e} f g. + +Section down. + Universes a b e e'. + Constraint e' < e. + Lemma funext_down {A B} + : @funext_type@{a b e} A B -> @funext_type@{a b e'} A B. + Proof. + intros H f g Hfg. exact (H f g Hfg). + Defined. +End down. diff --git a/test-suite/success/forward.v b/test-suite/success/forward.v index 0ed5b524f3..4e36dec15b 100644 --- a/test-suite/success/forward.v +++ b/test-suite/success/forward.v @@ -16,3 +16,14 @@ eremember (S (S ?[x])). instantiate (x:=0). reflexivity. Qed. + +(* Don't know if it is good or not but the compatibility tells that + the asserted goal to prove is subject to beta-iota but not the + asserted hypothesis *) + +Goal True. +assert ((fun x => x) False). +Fail match goal with |- (?f ?a) => idtac end. (* should be beta-iota reduced *) +2:match goal with _: (?f ?a) |- _ => idtac end. (* should not be beta-iota reduced *) +Abort. + diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 1d35f1ef6c..29e373eaa5 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -337,3 +337,14 @@ Goal True. evar (0=0). Abort. +(* Test location of hypothesis in "symmetry in H". This was broken in + 8.6 where H, when the oldest hyp, was moved at the place of most + recent hypothesis *) + +Goal 0=1 -> True -> True. +intros H H0. +symmetry in H. +(* H should be the first hypothesis *) +match goal with h:_ |- _ => assert (h=h) end. (* h should be H0 *) +exact (eq_refl H0). +Abort. |