diff options
Diffstat (limited to 'test-suite')
143 files changed, 2553 insertions, 156 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 5ab4cacdaf..ae426f0daf 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -27,12 +27,13 @@ # Default value when called from a freshly compiled Coq, but can be # easily overridden -LIB := $(shell cd ..; pwd) -BIN := $(LIB)/bin/ +LIB := .. +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`; \ @@ -170,6 +175,7 @@ summary.log: report: summary.log $(HIDE)./save-logs.sh $(HIDE)if [ -n "${TRAVIS}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo "travis_fold:start:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo "travis_fold:end:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';'; fi + $(HIDE)if [ -n "${APPVEYOR}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo {}' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo' ';'; fi $(HIDE)if grep -q -F 'Error!' summary.log ; then echo FAILURES; grep -F 'Error!' summary.log; false; else echo NO FAILURES; fi ####################################################################### @@ -293,7 +299,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) | grep -v "^<W>" \ | sed 's/File "[^"]*"/File "stdin"/' \ > $$tmpoutput; \ - diff -u $*.out $$tmpoutput 2>&1; R=$$?; times; \ + diff -u --strip-trailing-cr $*.out $$tmpoutput 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ @@ -328,7 +334,7 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out -e 's/\s*[-+]inf\s*//g' \ -e 's/^[^a-zA-Z]*//' \ $*.out | sort > $$tmpexpected; \ - diff -b -u $$tmpexpected $$tmpoutput 2>&1; R=$$?; times; \ + diff --strip-trailing-cr -b -u $$tmpexpected $$tmpoutput 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ @@ -445,7 +451,7 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake)) @echo "TEST $<" $(HIDE){ \ echo $(call log_intro,$<); \ - $(BIN)fake_ide $< "$(BIN)coqtop -coqlib $(LIB) -boot -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off" 2>&1; \ + $(BIN)fake_ide $< "-coqlib $(LIB) -boot -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off" 2>&1; \ if [ $$? = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ @@ -455,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 @@ -472,6 +480,8 @@ vio: $(patsubst %.v,%.vio.log,$(wildcard vio/*.v)) fi; \ } > "$@" +# coqchk + coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v)) %.chk.log:%.v @@ -488,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 @@ -504,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/2141.v b/test-suite/bugs/closed/2141.v index 098a7e9e72..c556ff0b2b 100644 --- a/test-suite/bugs/closed/2141.v +++ b/test-suite/bugs/closed/2141.v @@ -11,5 +11,6 @@ End FSetHide. Module NatSet' := FSetHide NatSet. Recursive Extraction NatSet'.fold. +Extraction TestCompile NatSet'.fold. (* Extraction "test2141.ml" NatSet'.fold. *)
\ No newline at end of file diff --git a/test-suite/bugs/closed/3287.v b/test-suite/bugs/closed/3287.v index 1b758acd73..4b3e7ff054 100644 --- a/test-suite/bugs/closed/3287.v +++ b/test-suite/bugs/closed/3287.v @@ -6,6 +6,7 @@ Definition bar := true. End Foo. Recursive Extraction Foo.bar. +Extraction TestCompile Foo.bar. Module Foo'. Definition foo := (I,I). @@ -13,10 +14,6 @@ Definition bar := true. End Foo'. Recursive Extraction Foo'.bar. +Extraction TestCompile Foo'.bar. -Module Foo''. -Definition foo := (I,I). -Definition bar := true. -End Foo''. - -Extraction Foo.bar. +Extraction Foo'.bar. diff --git a/test-suite/bugs/closed/3330.v b/test-suite/bugs/closed/3330.v index e3b5e94356..672fb3f131 100644 --- a/test-suite/bugs/closed/3330.v +++ b/test-suite/bugs/closed/3330.v @@ -41,6 +41,8 @@ Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function Open Scope function_scope. +Set Printing Universes. Set Printing All. + Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a. @@ -156,7 +158,8 @@ Delimit Scope morphism_scope with morphism. Delimit Scope category_scope with category. Delimit Scope object_scope with object. - +Set Printing Universes. +Set Printing All. Record PreCategory := Build_PreCategory' { object :> Type; @@ -1069,7 +1072,7 @@ Section Adjunction. Variable F : Functor C D. Variable G : Functor D C. - Let Adjunction_Type := + Let Adjunction_Type := Eval simpl in (hom_functor D) o (F^op, 1) <~=~> (hom_functor C) o (1, G). Record AdjunctionHom := diff --git a/test-suite/bugs/closed/3612.v b/test-suite/bugs/closed/3612.v index 73709268a4..33e5d532ad 100644 --- a/test-suite/bugs/closed/3612.v +++ b/test-suite/bugs/closed/3612.v @@ -39,7 +39,6 @@ Axiom path_path_sigma : forall {A : Type} (P : A -> Type) (u v : sigT P) p = q. Declare ML Module "ltac_plugin". -Declare ML Module "coretactics". Set Default Proof Mode "Classic". diff --git a/test-suite/bugs/closed/3649.v b/test-suite/bugs/closed/3649.v index 179f81e668..a664a1ef1d 100644 --- a/test-suite/bugs/closed/3649.v +++ b/test-suite/bugs/closed/3649.v @@ -3,7 +3,6 @@ (* coqc version trunk (September 2014) compiled on Sep 18 2014 21:0:5 with OCaml 4.01.0 coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *) Declare ML Module "ltac_plugin". -Declare ML Module "coretactics". Set Default Proof Mode "Classic". Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). Reserved Notation "x = y" (at level 70, no associativity). @@ -14,7 +13,6 @@ Axiom admit : forall {T}, T. Notation "A -> B" := (forall (_ : A), B) : type_scope. Reserved Infix "o" (at level 40, left associativity). Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope. -Ltac constr_eq a b := let test := constr:(@idpath _ _ : a = b) in idtac. Global Set Primitive Projections. Delimit Scope morphism_scope with morphism. Record PreCategory := diff --git a/test-suite/bugs/closed/3923.v b/test-suite/bugs/closed/3923.v index 2fb0a5439a..1d9488c6e1 100644 --- a/test-suite/bugs/closed/3923.v +++ b/test-suite/bugs/closed/3923.v @@ -33,3 +33,4 @@ Axiom empty_fieldstore : cert_fieldstore. End MkCertRuntimeTypes. Extraction MkCertRuntimeTypes. (* Was leading to an uncaught Not_found *) +Extraction TestCompile MkCertRuntimeTypes. diff --git a/test-suite/bugs/closed/3943.v b/test-suite/bugs/closed/3943.v new file mode 100644 index 0000000000..5e5ba816f9 --- /dev/null +++ b/test-suite/bugs/closed/3943.v @@ -0,0 +1,50 @@ +(* File reduced by coq-bug-finder from original input, then from 9492 lines to 119 lines *) +(* coqc version 8.5beta1 (January 2015) compiled on Jan 18 2015 7:27:36 with OCaml 3.12.1 + coqtop version 8.5beta1 (January 2015) *) + +Set Typeclasses Dependency Order. + +Inductive paths {A : Type} (a : A) : A -> Type := + idpath : paths a a. +Arguments idpath {A a} , [A] a. +Notation "x = y" := (@paths _ x y) : type_scope. +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y + := match p with idpath => idpath end. + +Set Implicit Arguments. +Delimit Scope morphism_scope with morphism. +Delimit Scope category_scope with category. +Delimit Scope object_scope with object. + +Record PreCategory := Build_PreCategory' { + object :> Type; + morphism : object -> object -> Type; + identity : forall x, morphism x x; + compose : forall s d d', + morphism d d' + -> morphism s d + -> morphism s d' }. +Arguments identity {!C%category} / x%object : rename. +Arguments compose {!C%category} / {s d d'}%object (m1 m2)%morphism : rename. + +Class IsIsomorphism {C : PreCategory} {s d} (m : morphism C s d) := { + morphism_inverse : morphism C d s; + left_inverse : compose morphism_inverse m = identity _; + right_inverse : compose m morphism_inverse = identity _ }. +Arguments morphism_inverse {C s d} m {_}. +Local Notation "m ^-1" := (morphism_inverse m) (at level 3, format "m '^-1'") : morphism_scope. + +Class Isomorphic {C : PreCategory} s d := { + morphism_isomorphic :> morphism C s d; + isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic }. +Coercion morphism_isomorphic : Isomorphic >-> morphism. + +Variable C : PreCategory. +Variables s d : C. + +Definition path_isomorphic (i j : Isomorphic s d) +: @morphism_isomorphic _ _ _ i = @morphism_isomorphic _ _ _ j -> i = j. +Admitted. + +Definition ap_morphism_inverse_path_isomorphic (i j : Isomorphic s d) p q +: ap (fun e : Isomorphic s d => e^-1)%morphism (path_isomorphic i j p) = q.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4250.v b/test-suite/bugs/closed/4250.v new file mode 100644 index 0000000000..74cacf559a --- /dev/null +++ b/test-suite/bugs/closed/4250.v @@ -0,0 +1,11 @@ +Require Import FunInd. +Require Vector. +Generalizable All Variables. + +Definition f `{n:nat , u:Vector.t A n} := n. + +Function f2 {A:Type} {n:nat} {v:Vector.t A n} : nat := n. + +(* fails with "The reference A was not found in the current environment." *) +Function f3 `{n:nat , u:Vector.t A n} := u. +Check R_f3_complete.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4366.v b/test-suite/bugs/closed/4366.v index 6a5e9a4023..403c2d2026 100644 --- a/test-suite/bugs/closed/4366.v +++ b/test-suite/bugs/closed/4366.v @@ -10,6 +10,6 @@ end. Goal True. Proof. pose (v := stupid 24). -Timeout 2 vm_compute in v. +Timeout 4 vm_compute in v. exact I. Qed. diff --git a/test-suite/bugs/closed/4616.v b/test-suite/bugs/closed/4616.v index a59975dbcf..d6660e3553 100644 --- a/test-suite/bugs/closed/4616.v +++ b/test-suite/bugs/closed/4616.v @@ -2,5 +2,6 @@ Require Coq.extraction.Extraction. Set Primitive Projections. Record Foo' := Foo { foo : Type }. -Axiom f : forall t : Foo', foo t. +Definition f := forall t : Foo', foo t. Extraction f. +Extraction TestCompile f. diff --git a/test-suite/bugs/closed/4709.v b/test-suite/bugs/closed/4709.v new file mode 100644 index 0000000000..a9edcc8043 --- /dev/null +++ b/test-suite/bugs/closed/4709.v @@ -0,0 +1,18 @@ + +(** Bug 4709 https://coq.inria.fr/bug/4709 + Extraction wasn't reducing primitive projections in types. *) + +Require Extraction. + +Set Primitive Projections. + +Record t := Foo { foo : Type }. +Definition ty := foo (Foo nat). + +(* Without proper reduction of primitive projections in + [extract_type], the type [ty] was extracted as [Tunknown]. + Let's check it isn't the case anymore. *) + +Parameter check : nat. +Extract Constant check => "(O:ty)". +Extraction TestCompile ty check. diff --git a/test-suite/bugs/closed/4710.v b/test-suite/bugs/closed/4710.v index 5d8ca330ac..e792a36234 100644 --- a/test-suite/bugs/closed/4710.v +++ b/test-suite/bugs/closed/4710.v @@ -4,7 +4,6 @@ Set Primitive Projections. Record Foo' := Foo { foo : nat }. Extraction foo. Record Foo2 (a : nat) := Foo2c { foo2p : nat; foo2b : bool }. -Extraction Language Ocaml. Extraction foo2p. Definition bla (x : Foo2 0) := foo2p _ x. @@ -12,3 +11,5 @@ Extraction bla. Definition bla' (a : nat) (x : Foo2 a) := foo2b _ x. Extraction bla'. + +Extraction TestCompile foo foo2p bla bla'. diff --git a/test-suite/bugs/closed/4720.v b/test-suite/bugs/closed/4720.v new file mode 100644 index 0000000000..704331e784 --- /dev/null +++ b/test-suite/bugs/closed/4720.v @@ -0,0 +1,50 @@ +(** Bug 4720 : extraction and "with" in module type *) + +Module Type A. + Parameter t : Set. +End A. + +Module A_instance <: A. + Definition t := nat. +End A_instance. + +Module A_private : A. + Definition t := nat. +End A_private. + +Module Type B. +End B. + +Module Type C (b : B). + Declare Module a : A. +End C. + +Module WithMod (a' : A) (b' : B) (c' : C b' with Module a := A_instance). +End WithMod. + +Module WithDef (a' : A) (b' : B) (c' : C b' with Definition a.t := nat). +End WithDef. + +Module WithModPriv (a' : A) (b' : B) (c' : C b' with Module a := A_private). +End WithModPriv. + +(* The initial bug report was concerning the extraction of WithModPriv + in Coq 8.4, which was suboptimal: it was compiling, but could have been + turned into some faulty code since A_private and c'.a were not seen as + identical by the extraction. + + In Coq 8.5 and 8.6, the extractions of WithMod, WithDef, WithModPriv + were all causing Anomaly or Assert Failure. This shoud be fixed now. +*) + +Require Extraction. + +Recursive Extraction WithMod. + +Recursive Extraction WithDef. + +Recursive Extraction WithModPriv. + +(* Let's even check that all this extracted code is actually compilable: *) + +Extraction TestCompile WithMod WithDef WithModPriv. diff --git a/test-suite/bugs/closed/4844.v b/test-suite/bugs/closed/4844.v new file mode 100644 index 0000000000..f140939ccd --- /dev/null +++ b/test-suite/bugs/closed/4844.v @@ -0,0 +1,47 @@ + +(* Bug report 4844 (and 4824): + The Haskell extraction was erroneously considering [Any] and + [()] as convertible ([Tunknown] an [Tdummy] internally). *) + +(* A value with inner logical parts. + Its extracted type will be [Sum () ()]. *) + +Definition semilogic : True + True := inl I. + +(* Higher-order record, whose projection [ST] isn't expressible + as an Haskell (or OCaml) type. Hence [ST] is extracted as the + unknown type [Any] in Haskell. *) + +Record SomeType := { ST : Type }. + +Definition SomeTrue := {| ST := True |}. + +(* A first version of the issue: + [abstrSum] is extracted as [Sum Any Any], so an unsafeCoerce + is required to cast [semilogic] into [abstrSum SomeTrue]. *) + +Definition abstrSum (t : SomeType) := ((ST t) + (ST t))%type. + +Definition semilogic' : abstrSum SomeTrue := semilogic. + +(* A deeper version of the issue. + In the previous example, the extraction could have reduced + [abstrSum SomeTrue] into [True+True], solving the issue. + It might do so in future versions. But if we put an inductive + in the way, a reduction isn't helpful. *) + +Inductive box (t : SomeType) := Box : ST t + ST t -> box t. + +Definition boxed_semilogic : box SomeTrue := + Box SomeTrue semilogic. + +Require Extraction. +Extraction Language Haskell. +Recursive Extraction semilogic' boxed_semilogic. +(* Warning! To fully check that this bug is still closed, + you should run ghc on the extracted code: + +Extraction "bug4844.hs" semilogic' boxed_semilogic. +ghc bug4844.hs + +*) diff --git a/test-suite/bugs/closed/5177.v b/test-suite/bugs/closed/5177.v new file mode 100644 index 0000000000..7c8af1e46e --- /dev/null +++ b/test-suite/bugs/closed/5177.v @@ -0,0 +1,22 @@ +(* Bug 5177 https://coq.inria.fr/bug/5177 : + Extraction and module type containing application and "with" *) + +Module Type T. + Parameter t: Type. +End T. + +Module Type A (MT: T). + Parameter t1: Type. + Parameter t2: Type. + Parameter bar: MT.t -> t1 -> t2. +End A. + +Module MakeA(MT: T): A MT with Definition t1 := nat. + Definition t1 := nat. + Definition t2 := nat. + Definition bar (m: MT.t) (x:t1) := x. +End MakeA. + +Require Extraction. +Recursive Extraction MakeA. +Extraction TestCompile MakeA. diff --git a/test-suite/bugs/closed/5205.v b/test-suite/bugs/closed/5205.v new file mode 100644 index 0000000000..406f37a4b1 --- /dev/null +++ b/test-suite/bugs/closed/5205.v @@ -0,0 +1,6 @@ +Definition foo (n : nat) (m : nat) : nat := m. + +Arguments foo {_} _, _ _. + +Check foo 1 1. +Check foo (n:=1) 1. diff --git a/test-suite/bugs/closed/5245.v b/test-suite/bugs/closed/5245.v new file mode 100644 index 0000000000..77bf169e18 --- /dev/null +++ b/test-suite/bugs/closed/5245.v @@ -0,0 +1,18 @@ +Set Primitive Projections. + +Record foo := Foo { + foo_car : Type; + foo_rel : foo_car -> foo_car -> Prop +}. +Arguments foo_rel : simpl never. + +Definition foo_fun {A B} := Foo (A -> B) (fun f g => forall x, f x = g x). + +Goal @foo_rel foo_fun (fun x : nat => x) (fun x => x). +Proof. +intros x; exact eq_refl. +Undo. +progress hnf; intros; exact eq_refl. +Undo. +unfold foo_rel. intros x. exact eq_refl. +Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/5315.v b/test-suite/bugs/closed/5315.v new file mode 100644 index 0000000000..f1f1b8c051 --- /dev/null +++ b/test-suite/bugs/closed/5315.v @@ -0,0 +1,10 @@ +Require Import Recdef. + +Function dumb_works (a:nat) {struct a} := + match (fun x => x) a with O => O | S n' => dumb_works n' end. + +Function dumb_nope (a:nat) {struct a} := + match (id (fun x => x)) a with O => O | S n' => dumb_nope n' end. + +(* This check is just present to ensure Function worked well *) +Check R_dumb_nope_complete.
\ No newline at end of file diff --git a/test-suite/bugs/closed/5365.v b/test-suite/bugs/closed/5365.v new file mode 100644 index 0000000000..be360d24d2 --- /dev/null +++ b/test-suite/bugs/closed/5365.v @@ -0,0 +1,13 @@ + +Inductive TupleT : nat -> Type := +| nilT : TupleT 0 +| consT {n} A : (A -> TupleT n) -> TupleT (S n). + +Inductive Tuple : forall n, TupleT n -> Type := + nil : Tuple _ nilT +| cons {n A} (x : A) (F : A -> TupleT n) : Tuple _ (F x) -> Tuple _ (consT A F). + +Inductive TupleMap : forall n, TupleT n -> TupleT n -> Type := + tmNil : TupleMap _ nilT nilT +| tmCons {n} {A B : Type} (F : A -> TupleT n) (G : B -> TupleT n) + : (forall x, sigT (fun y => TupleMap _ (F x) (G y))) -> TupleMap _ (consT A F) (consT B G). 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/5578.v b/test-suite/bugs/closed/5578.v new file mode 100644 index 0000000000..5bcdaa2f18 --- /dev/null +++ b/test-suite/bugs/closed/5578.v @@ -0,0 +1,57 @@ +(* File reduced by coq-bug-finder from original input, then from 1549 lines to 298 lines, then from 277 lines to 133 lines, then from 985 lines to 138 lines, then from 206 lines to 139 lines, then from 203 lines to 142 lines, then from 262 lines to 152 lines, then from 567 lines to 151 lines, then from 3746 lines to 151 lines, then from 577 lines to 151 lines, then from 187 lines to 151 lines, thenfrom 981 lines to 940 lines, then from 938 lines to 175 lines, then from 589 lines to 205 lines, then from 3797 lines to 205 lines, then from 628 lines to 206 lines, then from 238 lines to 205 lines, then from 1346 lines to 213 lines, then from 633 lines to 214 lines, then from 243 lines to 213 lines, then from 5656 lines to 245 lines, then from 661 lines to 272 lines, then from 3856 lines to 352 lines, then from 1266 lines to 407 lines, then from 421 lines to 406 lines, then from 424 lines to 91 lines, then from 105 lines to 91 lines, then from 85 lines to 55 lines, then from 69 lines to 55 lines *) +(* coqc version trunk (May 2017) compiled on May 30 2017 13:28:59 with OCaml +4.02.3 + coqtop version jgross-Leopard-WS:/home/jgross/Downloads/coq/coq-trunk,trunk (fd36c0451c26e44b1b7e93299d3367ad2d35fee3) *) + +Class Proper {A} (R : A -> A -> Prop) (m : A) := mkp : R m m. +Definition respectful {A B} (R : A -> A -> Prop) (R' : B -> B -> Prop) (f g : A -> B) := forall x y, R x y -> R' (f x) (g y). +Set Implicit Arguments. + +Class EqDec (A : Set) := { + eqb : A -> A -> bool ; + eqb_leibniz : forall x y, eqb x y = true <-> x = y +}. + +Infix "?=" := eqb (at level 70) : eq_scope. + +Inductive Comp : Set -> Type := +| Bind : forall (A B : Set), Comp B -> (B -> Comp A) -> Comp A. + +Open Scope eq_scope. + +Goal forall (Rat : Set) (PositiveMap_t : Set -> Set) + type (t : type) (interp_type_list_message interp_type_rand interp_type_message : nat -> Set), + (forall eta : nat, PositiveMap_t (interp_type_rand eta) -> interp_type_list_message eta -> interp_type_message eta) -> + ((nat -> Rat) -> Prop) -> + forall (interp_type_sbool : nat -> Set) (interp_type0 : type -> nat -> Set), + (forall eta : nat, + (interp_type_list_message eta -> interp_type_message eta) -> PositiveMap_t (interp_type_rand eta) -> interp_type0 t eta) + -> (forall (t0 : type) (eta : nat), EqDec (interp_type0 t0 eta)) + -> (bool -> Comp bool) -> False. + clear. + intros Rat PositiveMap_t type t interp_type_list_message interp_type_rand interp_type_message adv negligible interp_type_sbool + interp_type interp_term_fixed_t_x + EqDec_interp_type ret_bool. + assert (forall f adv' k + (lem : forall (eta : nat) (evil_rands rands : PositiveMap_t +(interp_type_rand eta)), + (interp_term_fixed_t_x eta (adv eta evil_rands) rands + ?= interp_term_fixed_t_x eta (adv eta evil_rands) rands) = true), + (forall (eta : nat), Proper (respectful eq eq) (f eta)) + -> negligible + (fun eta : nat => + f eta ( + (Bind (k eta) (fun rands => + ret_bool (interp_term_fixed_t_x eta (adv' eta) rands ?= interp_term_fixed_t_x eta (adv' eta) rands)))))). + Undo. + assert (forall f adv' k + (lem : forall (eta : nat) (rands : PositiveMap_t +(interp_type_rand eta)), + (interp_term_fixed_t_x eta (adv' eta) rands ?= interp_term_fixed_t_x eta (adv' eta) rands) = true), + (forall (eta : nat), Proper (respectful eq eq) (f eta)) + -> negligible + (fun eta : nat => + f eta ( + (Bind (k eta) (fun rands => + ret_bool (interp_term_fixed_t_x eta (adv' eta) rands ?= interp_term_fixed_t_x eta (adv' eta) rands)))))). + (* Error: Anomaly "Signature and its instance do not match." Please report at http://coq.inria.fr/bugs/. *)
\ No newline at end of file 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/5618.v b/test-suite/bugs/closed/5618.v new file mode 100644 index 0000000000..ab88a88f44 --- /dev/null +++ b/test-suite/bugs/closed/5618.v @@ -0,0 +1,9 @@ +Require Import FunInd. + +Function test {T} (v : T) (x : nat) : nat := + match x with + | 0 => 0 + | S x' => test v x' + end. + +Check R_test_complete.
\ No newline at end of file diff --git a/test-suite/bugs/closed/5641.v b/test-suite/bugs/closed/5641.v new file mode 100644 index 0000000000..9f3246f33d --- /dev/null +++ b/test-suite/bugs/closed/5641.v @@ -0,0 +1,6 @@ +Set Universe Polymorphism. + +Definition foo@{i j} (A : Type@{i}) : Type@{j}. +Proof. +abstract (exact ltac:(abstract (exact A))). +Defined. diff --git a/test-suite/bugs/closed/5671.v b/test-suite/bugs/closed/5671.v new file mode 100644 index 0000000000..c9a085045a --- /dev/null +++ b/test-suite/bugs/closed/5671.v @@ -0,0 +1,7 @@ +(* Fixing Meta-unclean specialize *) + +Require Import Setoid. +Axiom a : forall x, x=0 -> True. +Lemma lem (x y1 y2:nat) (H:x=0) (H0:eq y1 y2) : y1 = y2. +specialize a with (1:=H). clear H x. intros _. +setoid_rewrite H0. diff --git a/test-suite/bugs/closed/5683.v b/test-suite/bugs/closed/5683.v new file mode 100644 index 0000000000..b5c6a48ec0 --- /dev/null +++ b/test-suite/bugs/closed/5683.v @@ -0,0 +1,71 @@ +Require Import Program.Tactics. +Require Import FunctionalExtensionality. + +Inductive Succ A := +| Succ_O : Succ A +| Succ_S : A -> Succ A. +Arguments Succ_O {A}. +Arguments Succ_S {A} _. + +Inductive Zero : Type :=. + +Inductive ty := +| ty_nat : ty +| ty_arr : ty -> ty -> ty. + +Inductive term A := +| term_abs : ty -> term (Succ A) -> term A +| term_app : term A -> term A -> term A +| term_var : A -> term A +| term_nat : nat -> term A. +Arguments term_abs {A} _ _. +Arguments term_app {A} _ _. +Arguments term_var {A} _. +Arguments term_nat {A} _. + +Class Functor F := +{ + ret : forall {A}, A -> F A; + fmap : forall {A B}, (A -> B) -> F A -> F B; + fmap_id : forall {A} (fa : F A), fmap (@id A) fa = fa; + fmap_compose : forall {A B C} (fa : F A) (g : B -> C) (h : A -> B), fmap (fun +a => g (h a)) fa = fmap g (fmap h fa) +}. + +Class Monad M `{Functor M} := +{ + bind : forall {A B}, M A -> (A -> M B) -> M B; + ret_left_id : forall {A B} (a : A) (f : A -> M B), bind (ret a) f = f a; + ret_right_id : forall {A} (m : M A), bind m ret = m; + bind_assoc : forall {A B C} (m : M A) (f : A -> M B) (g : B -> M C), bind +(bind m f) g = bind m (fun x => bind (f x) g) +}. + +Instance Succ_Functor : Functor Succ. +Proof. + unshelve econstructor. + - intros A B f fa. + destruct fa. + + apply Succ_O. + + apply Succ_S. tauto. + - intros. apply Succ_S. assumption. + - intros A [|a]; reflexivity. + - intros A B C [|a] g h; reflexivity. +Defined. + +(* Anomaly: Not an arity *) +Program Fixpoint term_bind {A B} (tm : term A) (f : A -> term B) : term B := + let Succ_f (var : Succ A) := + match var with + | Succ_O => term_var Succ_O + | Succ_S var' => _ + end in + match tm with + | term_app tm1 tm2 => term_app (term_bind tm1 f) (term_bind tm2 f) + | term_abs ty body => term_abs ty (term_bind body Succ_f) + | term_var a => f a + | term_nat n => term_nat n + end. +Next Obligation. + intros. +Admitted. diff --git a/test-suite/bugs/closed/5697.v b/test-suite/bugs/closed/5697.v new file mode 100644 index 0000000000..c653f992af --- /dev/null +++ b/test-suite/bugs/closed/5697.v @@ -0,0 +1,19 @@ +Set Primitive Projections. + +Record foo : Type := Foo { foo_car: nat }. + +Goal forall x y : nat, x <> y -> Foo x <> Foo y. +Proof. +intros. +intros H'. +congruence. +Qed. + +Record bar (A : Type) : Type := Bar { bar_car: A }. + +Goal forall x y : nat, x <> y -> Bar nat x <> Bar nat y. +Proof. +intros. +intros H'. +congruence. +Qed. diff --git a/test-suite/bugs/closed/5713.v b/test-suite/bugs/closed/5713.v new file mode 100644 index 0000000000..9daf9647fc --- /dev/null +++ b/test-suite/bugs/closed/5713.v @@ -0,0 +1,15 @@ +(* Checking that classical_right/classical_left work in an empty context *) + +Require Import Classical. + +Parameter A:Prop. + +Goal A \/ ~A. +classical_right. +assumption. +Qed. + +Goal ~A \/ A. +classical_left. +assumption. +Qed. 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/bugs/closed/HoTT_coq_123.v b/test-suite/bugs/closed/HoTT_coq_123.v index cd9cad4064..7bed956f3e 100644 --- a/test-suite/bugs/closed/HoTT_coq_123.v +++ b/test-suite/bugs/closed/HoTT_coq_123.v @@ -104,11 +104,15 @@ Record Functor (C D : PreCategory) := morphism_of : forall s d, morphism C s d -> morphism D (object_of s) (object_of d) }. +(** Workaround to simpl losing universe constraints, see bug #5645. *) +Ltac simpl' := + simpl; match goal with [ |- ?P ] => let T := type of P in idtac end. + Global Instance trunc_forall `{Funext} `{P : A -> Type} `{forall a, IsTrunc n (P a)} : IsTrunc n (forall a, P a) | 100. Proof. generalize dependent P. - induction n as [ | n' IH]; (simpl; intros P ?). + induction n as [ | n' IH]; (simpl'; intros P ?). - admit. - pose (fun f g => trunc_equiv (@apD10 A P f g) ^-1); admit. Defined. diff --git a/test-suite/coq-makefile/arg/run.sh b/test-suite/coq-makefile/arg/run.sh index e98da17c78..e7de90ff2f 100755 --- a/test-suite/coq-makefile/arg/run.sh +++ b/test-suite/coq-makefile/arg/run.sh @@ -1,9 +1,7 @@ #!/usr/bin/env bash -#set -x -set -e - . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make diff --git a/test-suite/coq-makefile/compat-subdirs/run.sh b/test-suite/coq-makefile/compat-subdirs/run.sh index 28d9878f9b..221dcd7bf8 100755 --- a/test-suite/coq-makefile/compat-subdirs/run.sh +++ b/test-suite/coq-makefile/compat-subdirs/run.sh @@ -1,9 +1,8 @@ #!/usr/bin/env bash -#set -x -set -e - . ../template/init.sh + coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make exec test -f "subdir/done" diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh index e8291c89da..dc5a500db8 100755 --- a/test-suite/coq-makefile/coqdoc1/run.sh +++ b/test-suite/coq-makefile/coqdoc1/run.sh @@ -1,22 +1,21 @@ #!/usr/bin/env bash -#set -x -set -e - . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" make install-doc DSTROOT="$PWD/tmp" #make debug -(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual +(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual 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 e8291c89da..dc5a500db8 100755 --- a/test-suite/coq-makefile/coqdoc2/run.sh +++ b/test-suite/coq-makefile/coqdoc2/run.sh @@ -1,22 +1,21 @@ #!/usr/bin/env bash -#set -x -set -e - . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" make install-doc DSTROOT="$PWD/tmp" #make debug -(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual +(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual 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/extend-subdirs/run.sh b/test-suite/coq-makefile/extend-subdirs/run.sh index ea5792a937..221dcd7bf8 100755 --- a/test-suite/coq-makefile/extend-subdirs/run.sh +++ b/test-suite/coq-makefile/extend-subdirs/run.sh @@ -1,10 +1,8 @@ #!/usr/bin/env bash -#set -x -set -e - . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make exec test -f "subdir/done" 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..1615bfd067 --- /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..5b24df6397 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package/run.sh @@ -0,0 +1,18 @@ +#!/usr/bin/env bash + +. ../template/init.sh + +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 + export OCAMLPATH=`cygpath -w $PWD/findlib` +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/latex1/run.sh b/test-suite/coq-makefile/latex1/run.sh index 214a9d5b28..b2c5d5669b 100755 --- a/test-suite/coq-makefile/latex1/run.sh +++ b/test-suite/coq-makefile/latex1/run.sh @@ -1,13 +1,11 @@ #!/usr/bin/env bash -#set -x -set -e - if which pdflatex; then . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make exec make all.pdf diff --git a/test-suite/coq-makefile/merlin1/run.sh b/test-suite/coq-makefile/merlin1/run.sh index 752c0c2cea..1f262a9390 100755 --- a/test-suite/coq-makefile/merlin1/run.sh +++ b/test-suite/coq-makefile/merlin1/run.sh @@ -1,11 +1,9 @@ #!/usr/bin/env bash -#set -x -set -e - . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make .merlin cat > desired <<EOT B src diff --git a/test-suite/coq-makefile/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh index 10a200ddee..03df9cf050 100755 --- a/test-suite/coq-makefile/mlpack1/run.sh +++ b/test-suite/coq-makefile/mlpack1/run.sh @@ -1,22 +1,21 @@ #!/usr/bin/env bash -#set -x -set -e - . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib`; find .) | sort > actual +(cd `find tmp -name user-contrib` && find .) | sort > actual sort > desired <<EOT . ./test ./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 10a200ddee..03df9cf050 100755 --- a/test-suite/coq-makefile/mlpack2/run.sh +++ b/test-suite/coq-makefile/mlpack2/run.sh @@ -1,22 +1,21 @@ #!/usr/bin/env bash -#set -x -set -e - . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib`; find .) | sort > actual +(cd `find tmp -name user-contrib` && find .) | sort > actual sort > desired <<EOT . ./test ./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/multiroot/run.sh b/test-suite/coq-makefile/multiroot/run.sh index 3cd1ac305f..d3bb53106d 100755 --- a/test-suite/coq-makefile/multiroot/run.sh +++ b/test-suite/coq-makefile/multiroot/run.sh @@ -1,19 +1,17 @@ #!/usr/bin/env bash -#set -x -set -e - . ../template/init.sh cp -r theories theories2 mv src/test_plugin.mlpack src/test_plugin.mllib coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" make install-doc DSTROOT="$PWD/tmp" #make debug -(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual +(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual sort > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh index 9f6295d644..89bafe9ad1 100755 --- a/test-suite/coq-makefile/native1/run.sh +++ b/test-suite/coq-makefile/native1/run.sh @@ -1,25 +1,24 @@ #!/usr/bin/env bash -#set -x -set -e - NATIVECOMP=`grep "let no_native_compiler = false" ../../../config/coq_config.ml`||true if [[ `which ocamlopt` && $NATIVECOMP ]]; then . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib`; find .) | sort > actual +(cd `find tmp -name user-contrib` && find .) | sort > actual sort > desired <<EOT . ./test ./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/only/run.sh b/test-suite/coq-makefile/only/run.sh index 2ea3deffb7..8cf04bf2cd 100755 --- a/test-suite/coq-makefile/only/run.sh +++ b/test-suite/coq-makefile/only/run.sh @@ -1,11 +1,9 @@ #!/usr/bin/env bash -#set -x -set -e - . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make only TGTS="src/test.cmi src/test_aux.cmi" -j2 test -f src/test.cmi test -f src/test_aux.cmi diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh index 6301aa03c0..88606cd473 100755 --- a/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh +++ b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh @@ -27,6 +27,7 @@ let _ = Pre_env.empty_env EOT ${COQBIN}coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf if make VERBOSE=1; then # make command should have failed (but didn't) diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh index 991fb4a61d..939ef9c7b7 100755 --- a/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh +++ b/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh @@ -28,5 +28,6 @@ let _ = Pre_env.empty_env EOT ${COQBIN}coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make VERBOSE=1 diff --git a/test-suite/coq-makefile/plugin1/run.sh b/test-suite/coq-makefile/plugin1/run.sh index c2d47166fe..5433d9e92d 100755 --- a/test-suite/coq-makefile/plugin1/run.sh +++ b/test-suite/coq-makefile/plugin1/run.sh @@ -1,17 +1,15 @@ #!/usr/bin/env bash -#set -x -set -e - . ../template/init.sh mv src/test_plugin.mlpack src/test_plugin.mllib coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib`; find .) | sort > actual +(cd `find tmp -name user-contrib` && find .) | sort > actual sort > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/plugin2/run.sh b/test-suite/coq-makefile/plugin2/run.sh index c2d47166fe..5433d9e92d 100755 --- a/test-suite/coq-makefile/plugin2/run.sh +++ b/test-suite/coq-makefile/plugin2/run.sh @@ -1,17 +1,15 @@ #!/usr/bin/env bash -#set -x -set -e - . ../template/init.sh mv src/test_plugin.mlpack src/test_plugin.mllib coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib`; find .) | sort > actual +(cd `find tmp -name user-contrib` && find .) | sort > actual sort > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/plugin3/run.sh b/test-suite/coq-makefile/plugin3/run.sh index c2d47166fe..5433d9e92d 100755 --- a/test-suite/coq-makefile/plugin3/run.sh +++ b/test-suite/coq-makefile/plugin3/run.sh @@ -1,17 +1,15 @@ #!/usr/bin/env bash -#set -x -set -e - . ../template/init.sh mv src/test_plugin.mlpack src/test_plugin.mllib coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib`; find .) | sort > actual +(cd `find tmp -name user-contrib` && find .) | sort > actual sort > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/template/init.sh b/test-suite/coq-makefile/template/init.sh index c952d41a30..803fe8029a 100755 --- a/test-suite/coq-makefile/template/init.sh +++ b/test-suite/coq-makefile/template/init.sh @@ -1,3 +1,5 @@ +set -e +set -o pipefail export PATH=$COQBIN:$PATH diff --git a/test-suite/coq-makefile/timing/after/Fast.v b/test-suite/coq-makefile/timing/after/Fast.v new file mode 100644 index 0000000000..54d3cfc3eb --- /dev/null +++ b/test-suite/coq-makefile/timing/after/Fast.v @@ -0,0 +1,4 @@ +Require Coq.ZArith.BinInt. +Definition foo0 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. +Definition foo1 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. +Definition foo2 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. diff --git a/test-suite/coq-makefile/timing/after/Slow.v b/test-suite/coq-makefile/timing/after/Slow.v new file mode 100644 index 0000000000..8b13789179 --- /dev/null +++ b/test-suite/coq-makefile/timing/after/Slow.v @@ -0,0 +1 @@ + diff --git a/test-suite/coq-makefile/timing/after/_CoqProject b/test-suite/coq-makefile/timing/after/_CoqProject new file mode 100644 index 0000000000..36c3a18c2b --- /dev/null +++ b/test-suite/coq-makefile/timing/after/_CoqProject @@ -0,0 +1,2 @@ +Slow.v +Fast.v diff --git a/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired new file mode 100644 index 0000000000..729de2f366 --- /dev/null +++ b/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired @@ -0,0 +1,16 @@ +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +COQDEP Fast.v +COQDEP Slow.v +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +COQC Slow.v +Slow (real: 0.04, user: 0.02, sys: 0.01, mem: 45512 ko) +COQC Fast.v +Fast (real: 0.41, user: 0.37, sys: 0.04, mem: 395200 ko) +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' diff --git a/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired new file mode 100644 index 0000000000..b25bc3683c --- /dev/null +++ b/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired @@ -0,0 +1,16 @@ +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +COQDEP Fast.v +COQDEP Slow.v +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +COQC Slow.v +Slow (real: 0.40, user: 0.35, sys: 0.04, mem: 394968 ko) +COQC Fast.v +Fast (real: 0.04, user: 0.03, sys: 0.00, mem: 46564 ko) +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' diff --git a/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired new file mode 100644 index 0000000000..56815d241e --- /dev/null +++ b/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired @@ -0,0 +1,6 @@ +After | File Name | Before || Change | % Change +-------------------------------------------------------- +0m00.38s | Total | 0m00.39s || -0m00.01s | -2.56% +-------------------------------------------------------- +0m00.35s | Slow | 0m00.02s || +0m00.32s | +1649.99% +0m00.03s | Fast | 0m00.37s || -0m00.34s | -91.89%
\ No newline at end of file diff --git a/test-suite/coq-makefile/timing/aggregate/Fast.v b/test-suite/coq-makefile/timing/aggregate/Fast.v new file mode 100644 index 0000000000..8b13789179 --- /dev/null +++ b/test-suite/coq-makefile/timing/aggregate/Fast.v @@ -0,0 +1 @@ + diff --git a/test-suite/coq-makefile/timing/aggregate/Slow.v b/test-suite/coq-makefile/timing/aggregate/Slow.v new file mode 100644 index 0000000000..54d3cfc3eb --- /dev/null +++ b/test-suite/coq-makefile/timing/aggregate/Slow.v @@ -0,0 +1,4 @@ +Require Coq.ZArith.BinInt. +Definition foo0 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. +Definition foo1 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. +Definition foo2 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. diff --git a/test-suite/coq-makefile/timing/aggregate/_CoqProject b/test-suite/coq-makefile/timing/aggregate/_CoqProject new file mode 100644 index 0000000000..36c3a18c2b --- /dev/null +++ b/test-suite/coq-makefile/timing/aggregate/_CoqProject @@ -0,0 +1,2 @@ +Slow.v +Fast.v diff --git a/test-suite/coq-makefile/timing/before/Fast.v b/test-suite/coq-makefile/timing/before/Fast.v new file mode 100644 index 0000000000..8b13789179 --- /dev/null +++ b/test-suite/coq-makefile/timing/before/Fast.v @@ -0,0 +1 @@ + diff --git a/test-suite/coq-makefile/timing/before/Slow.v b/test-suite/coq-makefile/timing/before/Slow.v new file mode 100644 index 0000000000..54d3cfc3eb --- /dev/null +++ b/test-suite/coq-makefile/timing/before/Slow.v @@ -0,0 +1,4 @@ +Require Coq.ZArith.BinInt. +Definition foo0 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. +Definition foo1 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. +Definition foo2 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. diff --git a/test-suite/coq-makefile/timing/before/_CoqProject b/test-suite/coq-makefile/timing/before/_CoqProject new file mode 100644 index 0000000000..36c3a18c2b --- /dev/null +++ b/test-suite/coq-makefile/timing/before/_CoqProject @@ -0,0 +1,2 @@ +Slow.v +Fast.v diff --git a/test-suite/coq-makefile/timing/error/A.v b/test-suite/coq-makefile/timing/error/A.v new file mode 100644 index 0000000000..932363a122 --- /dev/null +++ b/test-suite/coq-makefile/timing/error/A.v @@ -0,0 +1 @@ +Check I : I. diff --git a/test-suite/coq-makefile/timing/error/_CoqProject b/test-suite/coq-makefile/timing/error/_CoqProject new file mode 100644 index 0000000000..790e057133 --- /dev/null +++ b/test-suite/coq-makefile/timing/error/_CoqProject @@ -0,0 +1 @@ +A.v diff --git a/test-suite/coq-makefile/timing/per-file-after/A.v b/test-suite/coq-makefile/timing/per-file-after/A.v new file mode 100644 index 0000000000..851e2b9738 --- /dev/null +++ b/test-suite/coq-makefile/timing/per-file-after/A.v @@ -0,0 +1,4 @@ +Require Coq.ZArith.BinInt. +Declare Reduction comp := native_compute. +Definition foo0 := Eval comp in (Coq.ZArith.BinInt.Z.div_eucl, Coq.ZArith.BinInt.Z.div_eucl). +Definition foo1 := Eval comp in (foo0, foo0). diff --git a/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired b/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired new file mode 100644 index 0000000000..18f0f34b28 --- /dev/null +++ b/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired @@ -0,0 +1,9 @@ +After | Code | Before || Change | % Change +--------------------------------------------------------------------------------------------------- +0m00.50s | Total | 0m04.17s || -0m03.66s | -87.96% +--------------------------------------------------------------------------------------------------- +0m00.145s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.192s || -0m00.04s | -24.47% +0m00.126s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.] | 0m00.143s || -0m00.01s | -11.88% + N/A | Chars 027 - 068 [Declare~Reduction~comp~:=~nati...] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] | N/A || +0m00.00s | N/A +0m00.231s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m03.836s || -0m03.60s | -93.97%
\ No newline at end of file diff --git a/test-suite/coq-makefile/timing/per-file-after/_CoqProject b/test-suite/coq-makefile/timing/per-file-after/_CoqProject new file mode 100644 index 0000000000..790e057133 --- /dev/null +++ b/test-suite/coq-makefile/timing/per-file-after/_CoqProject @@ -0,0 +1 @@ +A.v diff --git a/test-suite/coq-makefile/timing/per-file-before/A.v b/test-suite/coq-makefile/timing/per-file-before/A.v new file mode 100644 index 0000000000..115c1f95bd --- /dev/null +++ b/test-suite/coq-makefile/timing/per-file-before/A.v @@ -0,0 +1,4 @@ +Require Coq.ZArith.BinInt. +Declare Reduction comp := vm_compute. +Definition foo0 := Eval comp in (Coq.ZArith.BinInt.Z.div_eucl, Coq.ZArith.BinInt.Z.div_eucl). +Definition foo1 := Eval comp in (foo0, foo0). diff --git a/test-suite/coq-makefile/timing/per-file-before/_CoqProject b/test-suite/coq-makefile/timing/per-file-before/_CoqProject new file mode 100644 index 0000000000..790e057133 --- /dev/null +++ b/test-suite/coq-makefile/timing/per-file-before/_CoqProject @@ -0,0 +1 @@ +A.v diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh new file mode 100755 index 0000000000..9786af10a8 --- /dev/null +++ b/test-suite/coq-makefile/timing/run.sh @@ -0,0 +1,68 @@ +#!/usr/bin/env bash + +#set -x +set -e + +. ../template/init.sh + +cd error +coq_makefile -f _CoqProject -o Makefile +make cleanall +if make pretty-timed TGTS="all" -j1; then + echo "Error: make pretty-timed should have failed" + exit 1 +fi + +cd ../aggregate +coq_makefile -f _CoqProject -o Makefile +make cleanall +make pretty-timed TGTS="all" -j1 || exit $? + +cd ../before +coq_makefile -f _CoqProject -o Makefile +make cleanall +make make-pretty-timed-before TGTS="all" -j1 || exit $? + +cd ../after +coq_makefile -f _CoqProject -o Makefile +make cleanall +make make-pretty-timed-after TGTS="all" -j1 || exit $? +rm -f time-of-build-before.log +make print-pretty-timed-diff TIME_OF_BUILD_BEFORE_FILE=../before/time-of-build-before.log +cp ../before/time-of-build-before.log ./ +make print-pretty-timed-diff || exit $? + +for ext in "" .desired; do + for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do + cat ${file}${ext} | grep -v 'warning: undefined variable' | sed s'/[0-9]//g' | sed s'/ *$//g' | sed s'/^-*$/------/g' | sed s'/ */ /g' | sed s'/\(Total.*\)-\(.*\)-/\1+\2+/g' > ${file}${ext}.processed + done +done +for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do + diff -u $file.desired.processed $file.processed || exit $? +done + +cd ../per-file-before +coq_makefile -f _CoqProject -o Makefile +make cleanall +make all TIMING=before -j2 || exit $? + +cd ../per-file-after +coq_makefile -f _CoqProject -o Makefile +make cleanall +make all TIMING=after -j2 || exit $? + +find ../per-file-before/ -name "*.before-timing" -exec 'cp' '{}' './' ';' +make all.timing.diff -j2 || exit $? +cat A.v.timing.diff +echo + +for ext in "" .desired; do + for file in A.v.timing.diff; do + cat ${file}${ext} | sed s'/[0-9]*\.[0-9]*//g' | sed s'/0//g' | sed s'/ */ /g' | sed s'/+/-/g' | sort > ${file}${ext}.processed + done +done +for file in A.v.timing.diff; do + diff -u $file.desired.processed $file.processed || exit $? +done + +exit 0 diff --git a/test-suite/coq-makefile/uninstall1/run.sh b/test-suite/coq-makefile/uninstall1/run.sh index e525e12086..5354f794f7 100755 --- a/test-suite/coq-makefile/uninstall1/run.sh +++ b/test-suite/coq-makefile/uninstall1/run.sh @@ -1,11 +1,9 @@ #!/usr/bin/env bash -#set -x -set -e - . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" @@ -13,7 +11,7 @@ make install-doc DSTROOT="$PWD/tmp" make uninstall DSTROOT="$PWD/tmp" make uninstall-doc DSTROOT="$PWD/tmp" #make debug -(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual +(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual sort -u > desired <<EOT . EOT diff --git a/test-suite/coq-makefile/uninstall2/run.sh b/test-suite/coq-makefile/uninstall2/run.sh index e525e12086..5354f794f7 100755 --- a/test-suite/coq-makefile/uninstall2/run.sh +++ b/test-suite/coq-makefile/uninstall2/run.sh @@ -1,11 +1,9 @@ #!/usr/bin/env bash -#set -x -set -e - . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" @@ -13,7 +11,7 @@ make install-doc DSTROOT="$PWD/tmp" make uninstall DSTROOT="$PWD/tmp" make uninstall-doc DSTROOT="$PWD/tmp" #make debug -(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual +(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual sort -u > desired <<EOT . EOT diff --git a/test-suite/coq-makefile/validate1/run.sh b/test-suite/coq-makefile/validate1/run.sh index aaa4194b38..43bf39de10 100755 --- a/test-suite/coq-makefile/validate1/run.sh +++ b/test-suite/coq-makefile/validate1/run.sh @@ -1,10 +1,8 @@ #!/usr/bin/env bash -#set -x -set -e - . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make exec make validate diff --git a/test-suite/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v new file mode 100644 index 0000000000..7906a5b15e --- /dev/null +++ b/test-suite/coqchk/cumulativity.v @@ -0,0 +1,67 @@ +Set Universe Polymorphism. +Set Polymorphic Inductive Cumulativity. +Set Printing Universes. + +Inductive List (A: Type) := nil | cons : A -> List A -> List A. + +Section ListLift. + Universe i j. + + Constraint i < j. + + Definition LiftL {A} : List@{i} A -> List@{j} A := fun x => x. + +End ListLift. + +Lemma LiftL_Lem A (l : List A) : l = LiftL l. +Proof. reflexivity. Qed. + +Section ListLower. + Universe i j. + + Constraint i < j. + + Definition LowerL {A : Type@{i}} : List@{j} A -> List@{i} A := fun x => x. + +End ListLower. + +Lemma LowerL_Lem@{i j} (A : Type@{j}) (l : List@{i} A) : l = LowerL l. +Proof. reflexivity. Qed. +(* +I disable these tests because cqochk can't process them when compiled with + ocaml-4.02.3+32bit and camlp5-4.16 which is the case for Travis! + + I have added this file (including the commented parts below) in + test-suite/success/cumulativity.v which doesn't run coqchk on them. +*) +(* Inductive Tp := tp : Type -> Tp. *) + +(* Section TpLift. *) +(* Universe i j. *) + +(* Constraint i < j. *) + +(* Definition LiftTp : Tp@{i} -> Tp@{j} := fun x => x. *) + +(* End TpLift. *) + +(* Lemma LiftC_Lem (t : Tp) : LiftTp t = t. *) +(* Proof. reflexivity. Qed. *) + +(* Section TpLower. *) +(* Universe i j. *) + +(* Constraint i < j. *) + +(* Fail Definition LowerTp : Tp@{j} -> Tp@{i} := fun x => x. *) + +(* End TpLower. *) + + +(* Section subtyping_test. *) +(* Universe i j. *) +(* Constraint i < j. *) + +(* Inductive TP2 := tp2 : Type@{i} -> Type@{j} -> TP2. *) + +(* End subtyping_test. *)
\ No newline at end of file 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/bug5700.html.out b/test-suite/coqdoc/bug5700.html.out new file mode 100644 index 0000000000..0e05660d6c --- /dev/null +++ b/test-suite/coqdoc/bug5700.html.out @@ -0,0 +1,50 @@ +<!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.bug5700</title> +</head> + +<body> + +<div id="page"> + +<div id="header"> +</div> + +<div id="main"> + +<h1 class="libtitle">Library Coqdoc.bug5700</h1> + +<div class="code"> +</div> + +<div class="doc"> +<pre>foo (* bar *) </pre> + +</div> +<div class="code"> +<span class="id" title="keyword">Definition</span> <a name="const1"><span class="id" title="definition">const1</span></a> := 1.<br/> + +<br/> +</div> + +<div class="doc"> +<pre>more (* nested (* comments *) within verbatim *) </pre> + +</div> +<div class="code"> +<span class="id" title="keyword">Definition</span> <a name="const2"><span class="id" title="definition">const2</span></a> := 2.<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/bug5700.tex.out b/test-suite/coqdoc/bug5700.tex.out new file mode 100644 index 0000000000..33990cb89f --- /dev/null +++ b/test-suite/coqdoc/bug5700.tex.out @@ -0,0 +1,24 @@ +\documentclass[12pt]{report} +\usepackage[]{inputenc} +\usepackage[T1]{fontenc} +\usepackage{fullpage} +\usepackage{coqdoc} +\usepackage{amsmath,amssymb} +\usepackage{url} +\begin{document} +\coqlibrary{Coqdoc.bug5700}{Library }{Coqdoc.bug5700} + +\begin{coqdoccode} +\end{coqdoccode} +\begin{verbatim}foo (* bar *) \end{verbatim} + \begin{coqdoccode} +\coqdocnoindent +\coqdockw{Definition} \coqdef{Coqdoc.bug5700.const1}{const1}{\coqdocdefinition{const1}} := 1.\coqdoceol +\coqdocemptyline +\end{coqdoccode} +\begin{verbatim}more (* nested (* comments *) within verbatim *) \end{verbatim} + \begin{coqdoccode} +\coqdocnoindent +\coqdockw{Definition} \coqdef{Coqdoc.bug5700.const2}{const2}{\coqdocdefinition{const2}} := 2.\coqdoceol +\end{coqdoccode} +\end{document} diff --git a/test-suite/coqdoc/bug5700.v b/test-suite/coqdoc/bug5700.v new file mode 100644 index 0000000000..839034a48f --- /dev/null +++ b/test-suite/coqdoc/bug5700.v @@ -0,0 +1,5 @@ +(** << foo (* bar *) >> *) +Definition const1 := 1. + +(** << more (* nested (* comments *) within verbatim *) >> *) +Definition const2 := 2. 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/failure/Tauto.v b/test-suite/failure/Tauto.v index d91d159d9c..19976b41bd 100644 --- a/test-suite/failure/Tauto.v +++ b/test-suite/failure/Tauto.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/failure/clash_cons.v b/test-suite/failure/clash_cons.v index b3fbff680b..1761cc437d 100644 --- a/test-suite/failure/clash_cons.v +++ b/test-suite/failure/clash_cons.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/failure/fixpoint1.v b/test-suite/failure/fixpoint1.v index c2b521c214..0739982442 100644 --- a/test-suite/failure/fixpoint1.v +++ b/test-suite/failure/fixpoint1.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/failure/guard.v b/test-suite/failure/guard.v index 8db2785837..312dc48bea 100644 --- a/test-suite/failure/guard.v +++ b/test-suite/failure/guard.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/failure/illtype1.v b/test-suite/failure/illtype1.v index 8ed3af1ce4..fdd1bddd88 100644 --- a/test-suite/failure/illtype1.v +++ b/test-suite/failure/illtype1.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/failure/positivity.v b/test-suite/failure/positivity.v index 8089de2bf0..b21204b9e4 100644 --- a/test-suite/failure/positivity.v +++ b/test-suite/failure/positivity.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/failure/redef.v b/test-suite/failure/redef.v index c8dc6303f7..c49dbd7cae 100644 --- a/test-suite/failure/redef.v +++ b/test-suite/failure/redef.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/failure/search.v b/test-suite/failure/search.v index 648ab0820c..fae6cd6f3b 100644 --- a/test-suite/failure/search.v +++ b/test-suite/failure/search.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ideal-features/Apply.v b/test-suite/ideal-features/Apply.v index c8e9af216e..85680e94b9 100644 --- a/test-suite/ideal-features/Apply.v +++ b/test-suite/ideal-features/Apply.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/misc/deps-checksum.sh b/test-suite/misc/deps-checksum.sh index 1e2afb7540..e07612b84c 100755 --- a/test-suite/misc/deps-checksum.sh +++ b/test-suite/misc/deps-checksum.sh @@ -1,4 +1,4 @@ -rm -f misc/deps/*/*.vo +rm -f misc/deps/A/*.vo misc/deps/B/*.vo $coqc -R misc/deps/A A misc/deps/A/A.v $coqc -R misc/deps/B A misc/deps/B/A.v $coqc -R misc/deps/B A misc/deps/B/B.v diff --git a/test-suite/misc/deps-order.sh b/test-suite/misc/deps-order.sh index 375b706f0a..299f494693 100755 --- a/test-suite/misc/deps-order.sh +++ b/test-suite/misc/deps-order.sh @@ -1,10 +1,10 @@ # Check that both coqdep and coqtop/coqc supports -R # Check that both coqdep and coqtop/coqc takes the later -R # See bugs 2242, 2337, 2339 -rm -f misc/deps/*/*.vo +rm -f misc/deps/lib/*.vo misc/deps/client/*.vo tmpoutput=`mktemp /tmp/coqcheck.XXXXXX` $coqdep -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 | head -n 1 > $tmpoutput -diff -u misc/deps/deps.out $tmpoutput 2>&1 +diff -u --strip-trailing-cr misc/deps/deps.out $tmpoutput 2>&1 R=$? times $coqc -R misc/deps/lib lib misc/deps/lib/foo.v 2>&1 diff --git a/test-suite/misc/printers.sh b/test-suite/misc/printers.sh index c822d0eb37..28e7dc362f 100755 --- a/test-suite/misc/printers.sh +++ b/test-suite/misc/printers.sh @@ -1,3 +1,3 @@ -printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | grep Unbound +printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | egrep "Error|Unbound" if [ $? = 0 ]; then exit 1; else exit 0; fi diff --git a/test-suite/modules/polymorphism.v b/test-suite/modules/polymorphism.v new file mode 100644 index 0000000000..63eaa382dc --- /dev/null +++ b/test-suite/modules/polymorphism.v @@ -0,0 +1,81 @@ +Set Universe Polymorphism. + +(** Tests for module subtyping of polymorphic terms *) + +Module Type S. + +Section Foo. + +Universes i j. +Constraint i <= j. + +Parameter foo : Type@{i} -> Type@{j}. + +End Foo. + +End S. + +(** Same constraints *) + +Module OK_1. + +Definition foo@{i j} (A : Type@{i}) : Type@{j} := A. + +End OK_1. + +Module OK_1_Test : S := OK_1. + +(** More general constraints *) + +Module OK_2. + +Inductive X@{i} : Type@{i} :=. +Definition foo@{i j} (A : Type@{i}) : Type@{j} := X@{j}. + +End OK_2. + +Module OK_2_Test : S := OK_2. + +(** Wrong instance length *) + +Module KO_1. + +Definition foo@{i} (A : Type@{i}) : Type@{i} := A. + +End KO_1. + +Fail Module KO_Test_1 : S := KO_1. + +(** Less general constraints *) + +Module KO_2. + +Section Foo. + +Universe i j. +Constraint i < j. + +Definition foo (A : Type@{i}) : Type@{j} := A. + +End Foo. + +End KO_2. + +Fail Module KO_Test_2 : S := KO_2. + +(** Less general constraints *) + +Module KO_3. + +Section Foo. + +Universe i j. +Constraint i = j. + +Definition foo (A : Type@{i}) : Type@{j} := A. + +End Foo. + +End KO_3. + +Fail Module KO_Test_3 : S := KO_3. diff --git a/test-suite/modules/polymorphism2.v b/test-suite/modules/polymorphism2.v new file mode 100644 index 0000000000..7e3327eee0 --- /dev/null +++ b/test-suite/modules/polymorphism2.v @@ -0,0 +1,87 @@ +Set Universe Polymorphism. + +(** Tests for module subtyping of polymorphic terms *) + +Module Type S. + +Section Foo. + +Universes i j. +Constraint i <= j. + +Inductive foo : Type@{i} -> Type@{j} :=. + +End Foo. + +End S. + +(** Same constraints *) + +Module OK_1. + +Section Foo. + +Universes i j. +Constraint i <= j. + +Inductive foo : Type@{i} -> Type@{j} :=. + +End Foo. + +End OK_1. + +Module OK_1_Test : S := OK_1. + +(** More general constraints *) + +Module OK_2. + +Inductive foo@{i j} : Type@{i} -> Type@{j} :=. + +End OK_2. + +Module OK_2_Test : S := OK_2. + +(** Wrong instance length *) + +Module KO_1. + +Inductive foo@{i} : Type@{i} -> Type@{i} :=. + +End KO_1. + +Fail Module KO_Test_1 : S := KO_1. + +(** Less general constraints *) + +Module KO_2. + +Section Foo. + +Universe i j. +Constraint i < j. + +Inductive foo : Type@{i} -> Type@{j} :=. + +End Foo. + +End KO_2. + +Fail Module KO_Test_2 : S := KO_2. + +(** Less general constraints *) + +Module KO_3. + +Section Foo. + +Universe i j. +Constraint i = j. + +Inductive foo : Type@{i} -> Type@{j} :=. + +End Foo. + +End KO_3. + +Fail Module KO_Test_3 : S := KO_3. diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 9d106d2dac..7bcd7b041c 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -133,3 +133,5 @@ fun (x : nat) (p : x = x) => match p with | 1 => 1 end = p : forall x : nat, x = x -> Prop +bar 0 + : nat diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index 2ccca829d6..fe6c05c39e 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -1,3 +1,14 @@ +(* Bug 5568, don't warn for notations in repeated module import *) + +Module foo. +Notation compose := (fun g f => g f). +Notation "g & f" := (compose g f) (at level 10). +End foo. + +Import foo. +Import foo. +Import foo. + (**********************************************************************) (* Notations for if and let (submitted by Roland Zumkeller) *) @@ -280,3 +291,11 @@ Check fun (x:nat) (p : x=x) => match p with ONE => ONE end = p. Notation "1" := eq_refl. Check fun (x:nat) (p : x=x) => match p with 1 => 1 end = p. +(* Check bug 5693 *) + +Module M. +Definition A := 0. +Definition bar (a b : nat) := plus a b. +Notation "" := A (format "", only printing). +Check (bar A 0). +End M. diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index ffea0819a5..65efe228af 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,3 +111,16 @@ fun x : ?A => x === x : forall x : ?A, x = x where ?A : [x : ?A |- Type] (x cannot be used) +{{0, 1}} + : nat * nat +{{0, 1, 2}} + : nat * (nat * nat) +{{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 +!!! _ _ : nat, True + : (nat -> Prop) * ((nat -> Prop) * Prop) diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 250aecafd4..ea372ad1a3 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 ".." *) @@ -160,3 +165,28 @@ 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}}. + +(* 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. + +(* Test presence of notation variables in the recursive parts (introduced in dfdaf4de) *) +Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder). +Check !!! (x y:nat), True. diff --git a/test-suite/output/RecognizePluginWarning.out b/test-suite/output/RecognizePluginWarning.out new file mode 100644 index 0000000000..e69de29bb2 --- /dev/null +++ b/test-suite/output/RecognizePluginWarning.out diff --git a/test-suite/output/RecognizePluginWarning.v b/test-suite/output/RecognizePluginWarning.v new file mode 100644 index 0000000000..cd667bbd00 --- /dev/null +++ b/test-suite/output/RecognizePluginWarning.v @@ -0,0 +1,5 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "extraction-logical-axiom") -*- *) + +(* Test that mentioning a warning defined in plugins works. The failure +mode here is that these result in a warning about unknown warnings, since the +plugins are not known at command line parsing time. *) diff --git a/test-suite/output/TypeclassDebug.out b/test-suite/output/TypeclassDebug.out new file mode 100644 index 0000000000..8b38fe0ff4 --- /dev/null +++ b/test-suite/output/TypeclassDebug.out @@ -0,0 +1,18 @@ +Debug: 1: looking for foo without backtracking +Debug: 1.1: simple apply H on foo, 1 subgoal(s) +Debug: 1.1-1 : foo +Debug: 1.1-1: looking for foo without backtracking +Debug: 1.1-1.1: simple apply H on foo, 1 subgoal(s) +Debug: 1.1-1.1-1 : foo +Debug: 1.1-1.1-1: looking for foo without backtracking +Debug: 1.1-1.1-1.1: simple apply H on foo, 1 subgoal(s) +Debug: 1.1-1.1-1.1-1 : foo +Debug: 1.1-1.1-1.1-1: looking for foo without backtracking +Debug: 1.1-1.1-1.1-1.1: simple apply H on foo, 1 subgoal(s) +Debug: 1.1-1.1-1.1-1.1-1 : foo +Debug: 1.1-1.1-1.1-1.1-1: looking for foo without backtracking +Debug: 1.1-1.1-1.1-1.1-1.1: simple apply H on foo, 1 subgoal(s) +Debug: 1.1-1.1-1.1-1.1-1.1-1 : foo +The command has indeed failed with message: +Ltac call to "typeclasses eauto (int_or_var_opt) with (ne_preident_list)" failed. +Tactic failure: Proof search reached its limit. diff --git a/test-suite/output/TypeclassDebug.v b/test-suite/output/TypeclassDebug.v new file mode 100644 index 0000000000..d38e2a50e4 --- /dev/null +++ b/test-suite/output/TypeclassDebug.v @@ -0,0 +1,8 @@ +(* show alternating separators in typeclass debug output; see discussion in PR #868 *) + +Parameter foo : Prop. +Axiom H : foo -> foo. +Hint Resolve H : foo. +Goal foo. +Typeclasses eauto := debug. +Fail typeclasses eauto 5 with foo. 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/output/UsePluginWarning.out b/test-suite/output/UsePluginWarning.out new file mode 100644 index 0000000000..47409f3ec5 --- /dev/null +++ b/test-suite/output/UsePluginWarning.out @@ -0,0 +1 @@ +type foo = __ diff --git a/test-suite/output/UsePluginWarning.v b/test-suite/output/UsePluginWarning.v new file mode 100644 index 0000000000..c6e0054641 --- /dev/null +++ b/test-suite/output/UsePluginWarning.v @@ -0,0 +1,7 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "-extraction-logical-axiom") -*- *) + +Require Extraction. +Axiom foo : Prop. + +Extraction foo. + diff --git a/test-suite/output/Warnings.out b/test-suite/output/Warnings.out new file mode 100644 index 0000000000..a70f8ca45a --- /dev/null +++ b/test-suite/output/Warnings.out @@ -0,0 +1,3 @@ +File "stdin", line 4, characters 0-22: +Warning: Projection value has no head constant: fun x : B => x in canonical +instance a of b, ignoring it. [projection-no-head-constant,typechecker] diff --git a/test-suite/output/Warnings.v b/test-suite/output/Warnings.v new file mode 100644 index 0000000000..7465442cab --- /dev/null +++ b/test-suite/output/Warnings.v @@ -0,0 +1,5 @@ +(* Term in warning was not printed in the right environment at some time *) +Record A := { B:Type; b:B->B }. +Definition a B := {| B:=B; b:=fun x => x |}. +Canonical Structure a. + diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v index f761a4dc5a..73169dae65 100644 --- a/test-suite/output/inference.v +++ b/test-suite/output/inference.v @@ -14,6 +14,7 @@ Definition P (e:option L) := Print P. (* Check that plus is folded even if reduction is involved *) +Set Warnings Append "-deprecated-option". Set Refolding Reduction. Check (fun m n p (H : S m <= (S n) + p) => le_S_n _ _ H). diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v index e4ee351c3a..0f677a8495 100644 --- a/test-suite/success/Check.v +++ b/test-suite/success/Check.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/Field.v b/test-suite/success/Field.v index 438e461357..018b22c489 100644 --- a/test-suite/success/Field.v +++ b/test-suite/success/Field.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/FunindExtraction_compat86.v b/test-suite/success/FunindExtraction_compat86.v new file mode 100644 index 0000000000..8912197d2f --- /dev/null +++ b/test-suite/success/FunindExtraction_compat86.v @@ -0,0 +1,506 @@ +(* -*- coq-prog-args: ("-compat" "8.6") -*- *) + +Definition iszero (n : nat) : bool := + match n with + | O => true + | _ => false + end. + +Functional Scheme iszero_ind := Induction for iszero Sort Prop. + +Lemma toto : forall n : nat, n = 0 -> iszero n = true. +intros x eg. + functional induction iszero x; simpl. +trivial. +inversion eg. +Qed. + + +Function ftest (n m : nat) : nat := + match n with + | O => match m with + | O => 0 + | _ => 1 + end + | S p => 0 + end. +(* MS: FIXME: apparently can't define R_ftest_complete. Rest of the file goes through. *) + +Lemma test1 : forall n m : nat, ftest n m <= 2. +intros n m. + functional induction ftest n m; auto. +Qed. + +Lemma test2 : forall m n, ~ 2 = ftest n m. +Proof. +intros n m;intro H. +functional inversion H ftest. +Qed. + +Lemma test3 : forall n m, ftest n m = 0 -> (n = 0 /\ m = 0) \/ n <> 0. +Proof. +functional inversion 1 ftest;auto. +Qed. + + +Require Import Arith. +Lemma test11 : forall m : nat, ftest 0 m <= 2. +intros m. + functional induction ftest 0 m. +auto. +auto. +auto with *. +Qed. + +Function lamfix (m n : nat) {struct n } : nat := + match n with + | O => m + | S p => lamfix m p + end. + +(* Parameter v1 v2 : nat. *) + +Lemma lamfix_lem : forall v1 v2 : nat, lamfix v1 v2 = v1. +intros v1 v2. + functional induction lamfix v1 v2. +trivial. +assumption. +Defined. + + + +(* polymorphic function *) +Require Import List. + +Functional Scheme app_ind := Induction for app Sort Prop. + +Lemma appnil : forall (A : Set) (l l' : list A), l' = nil -> l = l ++ l'. +intros A l l'. + functional induction app A l l'; intuition. + rewrite <- H0; trivial. +Qed. + + + + + +Require Export Arith. + + +Function trivfun (n : nat) : nat := + match n with + | O => 0 + | S m => trivfun m + end. + + +(* essaie de parametre variables non locaux:*) + +Parameter varessai : nat. + +Lemma first_try : trivfun varessai = 0. + functional induction trivfun varessai. +trivial. +assumption. +Defined. + + + Functional Scheme triv_ind := Induction for trivfun Sort Prop. + +Lemma bisrepetita : forall n' : nat, trivfun n' = 0. +intros n'. + functional induction trivfun n'. +trivial. +assumption. +Qed. + + + + + + + +Function iseven (n : nat) : bool := + match n with + | O => true + | S (S m) => iseven m + | _ => false + end. + + +Function funex (n : nat) : nat := + match iseven n with + | true => n + | false => match n with + | O => 0 + | S r => funex r + end + end. + + +Function nat_equal_bool (n m : nat) {struct n} : bool := + match n with + | O => match m with + | O => true + | _ => false + end + | S p => match m with + | O => false + | S q => nat_equal_bool p q + end + end. + + +Require Export Div2. +Require Import Nat. +Functional Scheme div2_ind := Induction for div2 Sort Prop. +Lemma div2_inf : forall n : nat, div2 n <= n. +intros n. + functional induction div2 n. +auto. +auto. + +apply le_S. +apply le_n_S. +exact IHn0. +Qed. + +(* reuse this lemma as a scheme:*) + +Function nested_lam (n : nat) : nat -> nat := + match n with + | O => fun m : nat => 0 + | S n' => fun m : nat => m + nested_lam n' m + end. + + +Lemma nest : forall n m : nat, nested_lam n m = n * m. +intros n m. + functional induction nested_lam n m; simpl;auto. +Qed. + + +Function essai (x : nat) (p : nat * nat) {struct x} : nat := + let (n, m) := (p: nat*nat) in + match n with + | O => 0 + | S q => match x with + | O => 1 + | S r => S (essai r (q, m)) + end + end. + +Lemma essai_essai : + forall (x : nat) (p : nat * nat), let (n, m) := p in 0 < n -> 0 < essai x p. +intros x p. + functional induction essai x p; intros. +inversion H. +auto with arith. + auto with arith. +Qed. + +Function plus_x_not_five'' (n m : nat) {struct n} : nat := + let x := nat_equal_bool m 5 in + let y := 0 in + match n with + | O => y + | S q => + let recapp := plus_x_not_five'' q m in + match x with + | true => S recapp + | false => S recapp + end + end. + +Lemma notplusfive'' : forall x y : nat, y = 5 -> plus_x_not_five'' x y = x. +intros a b. + functional induction plus_x_not_five'' a b; intros hyp; simpl; auto. +Qed. + +Lemma iseq_eq : forall n m : nat, n = m -> nat_equal_bool n m = true. +intros n m. + functional induction nat_equal_bool n m; simpl; intros hyp; auto. +rewrite <- hyp in y; simpl in y;tauto. +inversion hyp. +Qed. + +Lemma iseq_eq' : forall n m : nat, nat_equal_bool n m = true -> n = m. +intros n m. + functional induction nat_equal_bool n m; simpl; intros eg; auto. +inversion eg. +inversion eg. +Qed. + + +Inductive istrue : bool -> Prop := + istrue0 : istrue true. + +Functional Scheme add_ind := Induction for add Sort Prop. + +Lemma inf_x_plusxy' : forall x y : nat, x <= x + y. +intros n m. + functional induction add n m; intros. +auto with arith. +auto with arith. +Qed. + + +Lemma inf_x_plusxy'' : forall x : nat, x <= x + 0. +intros n. +unfold plus. + functional induction plus n 0; intros. +auto with arith. +apply le_n_S. +assumption. +Qed. + +Lemma inf_x_plusxy''' : forall x : nat, x <= 0 + x. +intros n. + functional induction plus 0 n; intros; auto with arith. +Qed. + +Function mod2 (n : nat) : nat := + match n with + | O => 0 + | S (S m) => S (mod2 m) + | _ => 0 + end. + +Lemma princ_mod2 : forall n : nat, mod2 n <= n. +intros n. + functional induction mod2 n; simpl; auto with arith. +Qed. + +Function isfour (n : nat) : bool := + match n with + | S (S (S (S O))) => true + | _ => false + end. + +Function isononeorfour (n : nat) : bool := + match n with + | S O => true + | S (S (S (S O))) => true + | _ => false + end. + +Lemma toto'' : forall n : nat, istrue (isfour n) -> istrue (isononeorfour n). +intros n. + functional induction isononeorfour n; intros istr; simpl; + inversion istr. +apply istrue0. +destruct n. inversion istr. +destruct n. tauto. +destruct n. inversion istr. +destruct n. inversion istr. +destruct n. tauto. +simpl in *. inversion H0. +Qed. + +Lemma toto' : forall n m : nat, n = 4 -> istrue (isononeorfour n). +intros n. + functional induction isononeorfour n; intros m istr; inversion istr. +apply istrue0. +rewrite H in y; simpl in y;tauto. +Qed. + +Function ftest4 (n m : nat) : nat := + match n with + | O => match m with + | O => 0 + | S q => 1 + end + | S p => match m with + | O => 0 + | S r => 1 + end + end. + +Lemma test4 : forall n m : nat, ftest n m <= 2. +intros n m. + functional induction ftest n m; auto with arith. +Qed. + +Lemma test4' : forall n m : nat, ftest4 (S n) m <= 2. +intros n m. +assert ({n0 | n0 = S n}). +exists (S n);reflexivity. +destruct H as [n0 H1]. +rewrite <- H1;revert H1. + functional induction ftest4 n0 m. +inversion 1. +inversion 1. + +auto with arith. +auto with arith. +Qed. + +Function ftest44 (x : nat * nat) (n m : nat) : nat := + let (p, q) := (x: nat*nat) in + match n with + | O => match m with + | O => 0 + | S q => 1 + end + | S p => match m with + | O => 0 + | S r => 1 + end + end. + +Lemma test44 : + forall (pq : nat * nat) (n m o r s : nat), ftest44 pq n (S m) <= 2. +intros pq n m o r s. + functional induction ftest44 pq n (S m). +auto with arith. +auto with arith. +auto with arith. +auto with arith. +Qed. + +Function ftest2 (n m : nat) {struct n} : nat := + match n with + | O => match m with + | O => 0 + | S q => 0 + end + | S p => ftest2 p m + end. + +Lemma test2' : forall n m : nat, ftest2 n m <= 2. +intros n m. + functional induction ftest2 n m; simpl; intros; auto. +Qed. + +Function ftest3 (n m : nat) {struct n} : nat := + match n with + | O => 0 + | S p => match m with + | O => ftest3 p 0 + | S r => 0 + end + end. + +Lemma test3' : forall n m : nat, ftest3 n m <= 2. +intros n m. + functional induction ftest3 n m. +intros. +auto. +intros. +auto. +intros. +simpl. +auto. +Qed. + +Function ftest5 (n m : nat) {struct n} : nat := + match n with + | O => 0 + | S p => match m with + | O => ftest5 p 0 + | S r => ftest5 p r + end + end. + +Lemma test5 : forall n m : nat, ftest5 n m <= 2. +intros n m. + functional induction ftest5 n m. +intros. +auto. +intros. +auto. +intros. +simpl. +auto. +Qed. + +Function ftest7 (n : nat) : nat := + match ftest5 n 0 with + | O => 0 + | S r => 0 + end. + +Lemma essai7 : + forall (Hrec : forall n : nat, ftest5 n 0 = 0 -> ftest7 n <= 2) + (Hrec0 : forall n r : nat, ftest5 n 0 = S r -> ftest7 n <= 2) + (n : nat), ftest7 n <= 2. +intros hyp1 hyp2 n. + functional induction ftest7 n; auto. +Qed. + +Function ftest6 (n m : nat) {struct n} : nat := + match n with + | O => 0 + | S p => match ftest5 p 0 with + | O => ftest6 p 0 + | S r => ftest6 p r + end + end. + + +Lemma princ6 : + (forall n m : nat, n = 0 -> ftest6 0 m <= 2) -> + (forall n m p : nat, + ftest6 p 0 <= 2 -> ftest5 p 0 = 0 -> n = S p -> ftest6 (S p) m <= 2) -> + (forall n m p r : nat, + ftest6 p r <= 2 -> ftest5 p 0 = S r -> n = S p -> ftest6 (S p) m <= 2) -> + forall x y : nat, ftest6 x y <= 2. +intros hyp1 hyp2 hyp3 n m. +generalize hyp1 hyp2 hyp3. +clear hyp1 hyp2 hyp3. + functional induction ftest6 n m; auto. +Qed. + +Lemma essai6 : forall n m : nat, ftest6 n m <= 2. +intros n m. + functional induction ftest6 n m; simpl; auto. +Qed. + +(* Some tests with modules *) +Module M. +Function test_m (n:nat) : nat := + match n with + | 0 => 0 + | S n => S (S (test_m n)) + end. + +Lemma test_m_is_double : forall n, div2 (test_m n) = n. +Proof. +intros n. +functional induction (test_m n). +reflexivity. +simpl;rewrite IHn0;reflexivity. +Qed. +End M. +(* We redefine a new Function with the same name *) +Function test_m (n:nat) : nat := + pred n. + +Lemma test_m_is_pred : forall n, test_m n = pred n. +Proof. +intro n. +functional induction (test_m n). (* the test_m_ind to use is the last defined saying that test_m = pred*) +reflexivity. +Qed. + +(* Checks if the dot notation are correctly treated in infos *) +Lemma M_test_m_is_double : forall n, div2 (M.test_m n) = n. +intro n. +(* here we should apply M.test_m_ind *) +functional induction (M.test_m n). +reflexivity. +simpl;rewrite IHn0;reflexivity. +Qed. + +Import M. +(* Now test_m is the one which defines double *) + +Lemma test_m_is_double : forall n, div2 (M.test_m n) = n. +intro n. +(* here we should apply M.test_m_ind *) +functional induction (test_m n). +reflexivity. +simpl;rewrite IHn0;reflexivity. +Qed. + +Extraction iszero. diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v index 1abe14774c..6962e43e7e 100644 --- a/test-suite/success/Hints.v +++ b/test-suite/success/Hints.v @@ -37,7 +37,6 @@ Hint Resolve predf | 0 : predconv. Goal exists n, pred n. eexists. - Fail Timeout 1 typeclasses eauto with pred. Set Typeclasses Filtered Unification. Set Typeclasses Debug Verbosity 2. (* predf is not tried as it doesn't match the goal *) @@ -80,8 +79,6 @@ Qed. (** The other way around: goal contains redexes instead of instances *) Goal exists n, pred (0 + n). eexists. - (* predf is applied indefinitely *) - Fail Timeout 1 typeclasses eauto with pred. (* pred0 (pred _) matches the goal *) typeclasses eauto with predconv. Qed. @@ -169,8 +166,6 @@ Instance foo f : E (id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ f ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id). Proof. - Fail Timeout 1 apply _. (* 3.7s *) - Hint Cut [_* (a_is_b | b_is_c | c_is_d | d_is_e) (a_compose | b_compose | c_compose | d_compose | e_compose)] : typeclass_instances. diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index 837f2efd06..4d04f2cf9b 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -142,3 +142,8 @@ Fail Notation "'foobarkeyword'" := (@nil) (only parsing, only printing). Reserved Notation "x === y" (at level 50). Inductive EQ {A} (x:A) : A -> Prop := REFL : x === x where "x === y" := (EQ x y). + +(* Check that strictly ident or _ are coerced to a name *) + +Fail Check {x@{u},y|x=x}. +Fail Check {?[n],y|0=0}. diff --git a/test-suite/success/ROmega3.v b/test-suite/success/ROmega3.v new file mode 100644 index 0000000000..fd4ff260b5 --- /dev/null +++ b/test-suite/success/ROmega3.v @@ -0,0 +1,31 @@ + +Require Import ZArith ROmega. +Local Open Scope Z_scope. + +(** Benchmark provided by Chantal Keller, that romega used to + solve far too slowly (compared to omega or lia). *) + +Parameter v4 : Z. +Parameter v3 : Z. +Parameter o4 : Z. +Parameter s5 : Z. +Parameter v2 : Z. +Parameter o5 : Z. +Parameter s6 : Z. +Parameter v1 : Z. +Parameter o6 : Z. +Parameter s7 : Z. +Parameter v0 : Z. +Parameter o7 : Z. + +Lemma lemma_5833 : + ~ 16 * v4 + (8 * v3 + (-8192 * o4 + (-4096 * s5 + (4 * v2 + + (-4096 * o5 + (-2048 * s6 + (2 * v1 + (-2048 * o6 + + (-1024 * s7 + (v0 + -1024 * o7)))))))))) >= 8192 +\/ + 16 * v4 + (8 * v3 + (-8192 * o4 + (-4096 * s5 + (4 * v2 + + (-4096 * o5 + (-2048 * s6 + (2 * v1 + (-2048 * o6 + + (-1024 * s7 + (v0 + -1024 * o7)))))))))) >= 1024. +Proof. +Timeout 1 romega. (* should take a few milliseconds, not seconds *) +Timeout 1 Qed. (* ditto *) diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v index 767f15be72..bffd96044d 100644 --- a/test-suite/success/Tauto.v +++ b/test-suite/success/Tauto.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v index 023cb5f59d..87296744c4 100644 --- a/test-suite/success/TestRefine.v +++ b/test-suite/success/TestRefine.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/abstract_poly.v b/test-suite/success/abstract_poly.v new file mode 100644 index 0000000000..b736b734fd --- /dev/null +++ b/test-suite/success/abstract_poly.v @@ -0,0 +1,20 @@ +Set Universe Polymorphism. + +Inductive path@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := refl : path x x. +Inductive unit@{i} : Type@{i} := tt. + +Lemma foo@{i j} : forall (m n : unit@{i}) (P : unit -> Type@{j}), path m n -> P m -> P n. +Proof. +intros m n P e p. +abstract (rewrite e in p; exact p). +Defined. + +Check foo_subproof@{Set Set}. + +Lemma bar : forall (m n : unit) (P : unit -> Type), path m n -> P m -> P n. +Proof. +intros m n P e p. +abstract (rewrite e in p; exact p). +Defined. + +Check bar_subproof@{Set Set Set}. diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v new file mode 100644 index 0000000000..0ee85712e2 --- /dev/null +++ b/test-suite/success/cumulativity.v @@ -0,0 +1,100 @@ +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 Polymorphic Inductive Cumulativity. +Set Printing Universes. + +Inductive List (A: Type) := nil | cons : A -> List A -> List A. + +Section ListLift. + Universe i j. + + Constraint i < j. + + Definition LiftL {A} : List@{i} A -> List@{j} A := fun x => x. + +End ListLift. + +Lemma LiftL_Lem A (l : List A) : l = LiftL l. +Proof. reflexivity. Qed. + +Section ListLower. + Universe i j. + + Constraint i < j. + + Definition LowerL {A : Type@{i}} : List@{j} A -> List@{i} A := fun x => x. + +End ListLower. + +Lemma LowerL_Lem@{i j} (A : Type@{j}) (l : List@{i} A) : l = LowerL l. +Proof. reflexivity. Qed. + +Inductive Tp := tp : Type -> Tp. + +Section TpLift. + Universe i j. + + Constraint i < j. + + Definition LiftTp : Tp@{i} -> Tp@{j} := fun x => x. + +End TpLift. + +Lemma LiftC_Lem (t : Tp) : LiftTp t = t. +Proof. reflexivity. Qed. + +Section TpLower. + Universe i j. + + Constraint i < j. + + Fail Definition LowerTp : Tp@{j} -> Tp@{i} := fun x => x. + +End TpLower. + + +Section subtyping_test. + Universe i j. + Constraint i < j. + + Inductive TP2 := tp2 : Type@{i} -> Type@{j} -> TP2. + +End subtyping_test. + +Record A : Type := { a :> Type; }. + +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/eauto.v b/test-suite/success/eauto.v index 160f2d9deb..9b0ff1c8fe 100644 --- a/test-suite/success/eauto.v +++ b/test-suite/success/eauto.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/eqdecide.v b/test-suite/success/eqdecide.v index 724e2998ef..055434df01 100644 --- a/test-suite/success/eqdecide.v +++ b/test-suite/success/eqdecide.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v index 89be144152..0ee2232502 100644 --- a/test-suite/success/extraction.v +++ b/test-suite/success/extraction.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -545,47 +545,96 @@ Recursive Extraction test_proj. (*** TO SUM UP: ***) -(* Was previously producing a "test_extraction.ml" *) -Recursive Extraction - idnat id id' test2 test3 test4 test5 test6 test7 d d2 - d3 d4 d5 d6 test8 id id' test9 test10 test11 test12 - test13 test19 test20 nat sumbool_rect c Finite tree - tree_size test14 test15 eta_c test16 test17 test18 bidon - tb fbidon fbidon2 fbidon2 test_0 test_1 eq eq_rect tp1 - tp1bis Truc oups test24 loop horibilis PropSet natbool - zerotrue zeroTrue zeroprop test21 test22 test23 f f_prop - f_arity f_normal Boite boite1 boite2 test_boite Box box1 - zarb test_proj. +Module Everything. + Definition idnat := idnat. + Definition id := id. + Definition id' := id'. + Definition test2 := test2. + Definition test3 := test3. + Definition test4 := test4. + Definition test5 := test5. + Definition test6 := test6. + Definition test7 := test7. + Definition d := d. + Definition d2 := d2. + Definition d3 := d3. + Definition d4 := d4. + Definition d5 := d5. + Definition d6 := d6. + Definition test8 := test8. + Definition test9 := test9. + Definition test10 := test10. + Definition test11 := test11. + Definition test12 := test12. + Definition test13 := test13. + Definition test19 := test19. + Definition test20 := test20. + Definition nat := nat. + Definition sumbool_rect := sumbool_rect. + Definition c := c. + Definition Finite := Finite. + Definition tree := tree. + Definition tree_size := tree_size. + Definition test14 := test14. + Definition test15 := test15. + Definition eta_c := eta_c. + Definition test16 := test16. + Definition test17 := test17. + Definition test18 := test18. + Definition bidon := bidon. + Definition tb := tb. + Definition fbidon := fbidon. + Definition fbidon2 := fbidon2. + Definition test_0 := test_0. + Definition test_1 := test_1. + Definition eq_rect := eq_rect. + Definition tp1 := tp1. + Definition tp1bis := tp1bis. + Definition Truc := Truc. + Definition oups := oups. + Definition test24 := test24. + Definition loop := loop. + Definition horibilis := horibilis. + Definition PropSet := PropSet. + Definition natbool := natbool. + Definition zerotrue := zerotrue. + Definition zeroTrue := zeroTrue. + Definition zeroprop := zeroprop. + Definition test21 := test21. + Definition test22 := test22. + Definition test23 := test23. + Definition f := f. + Definition f_prop := f_prop. + Definition f_arity := f_arity. + Definition f_normal := f_normal. + Definition Boite := Boite. + Definition boite1 := boite1. + Definition boite2 := boite2. + Definition test_boite := test_boite. + Definition Box := Box. + Definition box1 := box1. + Definition zarb := zarb. + Definition test_proj := test_proj. +End Everything. + +(* Extraction "test_extraction.ml" Everything. *) +Recursive Extraction Everything. +(* Check that the previous OCaml code is compilable *) +Extraction TestCompile Everything. Extraction Language Haskell. -(* Was previously producing a "Test_extraction.hs" *) -Recursive Extraction - idnat id id' test2 test3 test4 test5 test6 test7 d d2 - d3 d4 d5 d6 test8 id id' test9 test10 test11 test12 - test13 test19 test20 nat sumbool_rect c Finite tree - tree_size test14 test15 eta_c test16 test17 test18 bidon - tb fbidon fbidon2 fbidon2 test_0 test_1 eq eq_rect tp1 - tp1bis Truc oups test24 loop horibilis PropSet natbool - zerotrue zeroTrue zeroprop test21 test22 test23 f f_prop - f_arity f_normal Boite boite1 boite2 test_boite Box box1 - zarb test_proj. +(* Extraction "Test_extraction.hs" Everything. *) +Recursive Extraction Everything. Extraction Language Scheme. -(* Was previously producing a "test_extraction.scm" *) -Recursive Extraction - idnat id id' test2 test3 test4 test5 test6 test7 d d2 - d3 d4 d5 d6 test8 id id' test9 test10 test11 test12 - test13 test19 test20 nat sumbool_rect c Finite tree - tree_size test14 test15 eta_c test16 test17 test18 bidon - tb fbidon fbidon2 fbidon2 test_0 test_1 eq eq_rect tp1 - tp1bis Truc oups test24 loop horibilis PropSet natbool - zerotrue zeroTrue zeroprop test21 test22 test23 f f_prop - f_arity f_normal Boite boite1 boite2 test_boite Box box1 - zarb test_proj. +(* Extraction "test_extraction.scm" Everything. *) +Recursive Extraction Everything. (*** Finally, a test more focused on everyday's life situations ***) Require Import ZArith. -Recursive Extraction two_or_two_plus_one Zdiv_eucl_exist. +Extraction Language Ocaml. +Recursive Extraction Z_modulo_2 Zdiv_eucl_exist. +Extraction TestCompile Z_modulo_2 Zdiv_eucl_exist. diff --git a/test-suite/success/extraction_dep.v b/test-suite/success/extraction_dep.v index e770cf779a..fb0adabae9 100644 --- a/test-suite/success/extraction_dep.v +++ b/test-suite/success/extraction_dep.v @@ -4,7 +4,7 @@ Require Coq.extraction.Extraction. (** NB: we should someday check the produced code instead of - simply running the commands. *) + extracting and just compiling. *) (** 1) Without signature ... *) @@ -20,6 +20,7 @@ End A. Definition testA := A.u + A.B.x. Recursive Extraction testA. (* without: v w *) +Extraction TestCompile testA. (** 1b) Same with an Include *) @@ -31,6 +32,7 @@ End Abis. Definition testAbis := Abis.u + Abis.y. Recursive Extraction testAbis. (* without: A B v w x *) +Extraction TestCompile testAbis. (** 2) With signature, we only keep elements mentionned in signature. *) @@ -46,3 +48,4 @@ End Ater. Definition testAter := Ater.u. Recursive Extraction testAter. (* with only: u v *) +Extraction TestCompile testAter. diff --git a/test-suite/success/extraction_impl.v b/test-suite/success/extraction_impl.v index 5bf807b1c6..a38a688fb4 100644 --- a/test-suite/success/extraction_impl.v +++ b/test-suite/success/extraction_impl.v @@ -2,7 +2,7 @@ (** Examples of extraction with manually-declared implicit arguments *) (** NB: we should someday check the produced code instead of - simply running the commands. *) + extracting and just compiling. *) Require Coq.extraction.Extraction. @@ -22,9 +22,11 @@ Proof. Defined. Recursive Extraction dnat_nat. +Extraction TestCompile dnat_nat. Extraction Implicit dnat_nat [n]. Recursive Extraction dnat_nat. +Extraction TestCompile dnat_nat. (** Same, with a Fixpoint *) @@ -35,9 +37,11 @@ Fixpoint dnat_nat' n (d:dnat n) := end. Recursive Extraction dnat_nat'. +Extraction TestCompile dnat_nat'. Extraction Implicit dnat_nat' [n]. Recursive Extraction dnat_nat'. +Extraction TestCompile dnat_nat'. (** Bug #4243, part 2 *) @@ -56,6 +60,7 @@ Defined. Extraction Implicit es [n]. Extraction Implicit enat_nat [n]. Recursive Extraction enat_nat. +Extraction TestCompile enat_nat. (** Same, with a Fixpoint *) @@ -67,6 +72,7 @@ Fixpoint enat_nat' n (e:enat n) : nat := Extraction Implicit enat_nat' [n]. Recursive Extraction enat_nat'. +Extraction TestCompile enat_nat'. (** Bug #4228 *) @@ -82,3 +88,4 @@ Extraction Implicit two_course [n]. End Food. Recursive Extraction Food.Meal. +Extraction TestCompile Food.Meal. 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/inds_type_sec.v b/test-suite/success/inds_type_sec.v index c729b23ce7..7e9095dfd7 100644 --- a/test-suite/success/inds_type_sec.v +++ b/test-suite/success/inds_type_sec.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index 1ed731f50f..35d7929877 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) 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. diff --git a/test-suite/success/mutual_ind.v b/test-suite/success/mutual_ind.v index 45c1a5e584..c4c5623897 100644 --- a/test-suite/success/mutual_ind.v +++ b/test-suite/success/mutual_ind.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index 66ff55edcb..ecc988507c 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -352,3 +352,35 @@ Module Anonymous. Check collapsethemiddle@{_ _}. End Anonymous. + +Module F. + Context {A B : Type}. + Definition foo : Type := B. +End F. + +Set Universe Polymorphism. + +Cumulative Record box (X : Type) (T := Type) : Type := wrap { unwrap : T }. + +Section test_letin_subtyping. + Universe i j k i' j' k'. + Constraint j < j'. + + Context (W : Type) (X : box@{i j k} W). + Definition Y := X : box@{i' j' k'} W. + + Universe i1 j1 k1 i2 j2 k2. + Constraint i1 < i2. + Constraint k2 < k1. + Context (V : Type). + + Definition Z : box@{i1 j1 k1} V := {| unwrap := V |}. + Definition Z' : box@{i2 j2 k2} V := {| unwrap := V |}. + Lemma ZZ' : @eq (box@{i2 j2 k2} V) Z Z'. + Proof. + Set Printing All. Set Printing Universes. + cbv. + reflexivity. + Qed. + +End test_letin_subtyping. diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v index 789854b2d6..576bdbf71b 100644 --- a/test-suite/success/primitiveproj.v +++ b/test-suite/success/primitiveproj.v @@ -184,6 +184,7 @@ Definition term' (x : wrap nat) := let f := (@unwrap2 nat) in f x. Require Coq.extraction.Extraction. Recursive Extraction term term'. +Extraction TestCompile term term'. (*Unset Printing Primitive Projection Parameters.*) (* Primitive projections in the presence of let-ins (was not failing in beta3)*) diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v index d595cbc2b8..ce1c33fc40 100644 --- a/test-suite/success/unfold.v +++ b/test-suite/success/unfold.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/typeclasses/NewSetoid.v b/test-suite/typeclasses/NewSetoid.v index 49f20a23f5..37d197a15c 100644 --- a/test-suite/typeclasses/NewSetoid.v +++ b/test-suite/typeclasses/NewSetoid.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |