aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/bugs/closed/5245.v18
-rw-r--r--test-suite/bugs/closed/5683.v71
-rw-r--r--test-suite/bugs/closed/5697.v19
-rwxr-xr-xtest-suite/coq-makefile/coqdoc1/run.sh1
-rwxr-xr-xtest-suite/coq-makefile/coqdoc2/run.sh1
-rw-r--r--test-suite/coq-makefile/findlib-package/Makefile.local1
-rw-r--r--test-suite/coq-makefile/findlib-package/_CoqProject10
-rw-r--r--test-suite/coq-makefile/findlib-package/findlib/foo/META4
-rw-r--r--test-suite/coq-makefile/findlib-package/findlib/foo/Makefile14
-rw-r--r--test-suite/coq-makefile/findlib-package/findlib/foo/foo.mli0
-rw-r--r--test-suite/coq-makefile/findlib-package/findlib/foo/foolib.ml2
-rwxr-xr-xtest-suite/coq-makefile/findlib-package/run.sh18
-rwxr-xr-xtest-suite/coq-makefile/mlpack1/run.sh1
-rwxr-xr-xtest-suite/coq-makefile/mlpack2/run.sh1
-rwxr-xr-xtest-suite/coq-makefile/native1/run.sh1
-rw-r--r--test-suite/coqdoc/bug5700.html.out50
-rw-r--r--test-suite/coqdoc/bug5700.tex.out24
-rw-r--r--test-suite/coqdoc/bug5700.v5
18 files changed, 241 insertions, 0 deletions
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/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/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh
index 1feff7479b..dc5a500db8 100755
--- a/test-suite/coq-makefile/coqdoc1/run.sh
+++ b/test-suite/coq-makefile/coqdoc1/run.sh
@@ -15,6 +15,7 @@ sort -u > desired <<EOT
./test
./test/test_plugin.cmi
./test/test_plugin.cmx
+./test/test_plugin.cmxa
./test/test_plugin.cmxs
./test/test.glob
./test/test.v
diff --git a/test-suite/coq-makefile/coqdoc2/run.sh b/test-suite/coq-makefile/coqdoc2/run.sh
index 1feff7479b..dc5a500db8 100755
--- a/test-suite/coq-makefile/coqdoc2/run.sh
+++ b/test-suite/coq-makefile/coqdoc2/run.sh
@@ -15,6 +15,7 @@ sort -u > desired <<EOT
./test
./test/test_plugin.cmi
./test/test_plugin.cmx
+./test/test_plugin.cmxa
./test/test_plugin.cmxs
./test/test.glob
./test/test.v
diff --git a/test-suite/coq-makefile/findlib-package/Makefile.local b/test-suite/coq-makefile/findlib-package/Makefile.local
new file mode 100644
index 0000000000..0f4a7d9954
--- /dev/null
+++ b/test-suite/coq-makefile/findlib-package/Makefile.local
@@ -0,0 +1 @@
+CAMLPKGS += -package foo
diff --git a/test-suite/coq-makefile/findlib-package/_CoqProject b/test-suite/coq-makefile/findlib-package/_CoqProject
new file mode 100644
index 0000000000..69f47302e1
--- /dev/null
+++ b/test-suite/coq-makefile/findlib-package/_CoqProject
@@ -0,0 +1,10 @@
+-R src test
+-R theories test
+-I src
+
+src/test_plugin.mlpack
+src/test.ml4
+src/test.mli
+src/test_aux.ml
+src/test_aux.mli
+theories/test.v
diff --git a/test-suite/coq-makefile/findlib-package/findlib/foo/META b/test-suite/coq-makefile/findlib-package/findlib/foo/META
new file mode 100644
index 0000000000..ff5f1c7c96
--- /dev/null
+++ b/test-suite/coq-makefile/findlib-package/findlib/foo/META
@@ -0,0 +1,4 @@
+archive(byte)="foo.cma"
+archive(native)="foo.cmxa"
+linkopts="-linkall"
+requires="str"
diff --git a/test-suite/coq-makefile/findlib-package/findlib/foo/Makefile b/test-suite/coq-makefile/findlib-package/findlib/foo/Makefile
new file mode 100644
index 0000000000..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/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh
index 51669f28f5..03df9cf050 100755
--- a/test-suite/coq-makefile/mlpack1/run.sh
+++ b/test-suite/coq-makefile/mlpack1/run.sh
@@ -15,6 +15,7 @@ sort > desired <<EOT
./test/test.glob
./test/test_plugin.cmi
./test/test_plugin.cmx
+./test/test_plugin.cmxa
./test/test_plugin.cmxs
./test/test.v
./test/test.vo
diff --git a/test-suite/coq-makefile/mlpack2/run.sh b/test-suite/coq-makefile/mlpack2/run.sh
index 51669f28f5..03df9cf050 100755
--- a/test-suite/coq-makefile/mlpack2/run.sh
+++ b/test-suite/coq-makefile/mlpack2/run.sh
@@ -15,6 +15,7 @@ sort > desired <<EOT
./test/test.glob
./test/test_plugin.cmi
./test/test_plugin.cmx
+./test/test_plugin.cmxa
./test/test_plugin.cmxs
./test/test.v
./test/test.vo
diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh
index 3bec11cb75..89bafe9ad1 100755
--- a/test-suite/coq-makefile/native1/run.sh
+++ b/test-suite/coq-makefile/native1/run.sh
@@ -18,6 +18,7 @@ sort > desired <<EOT
./test/test.glob
./test/test_plugin.cmi
./test/test_plugin.cmx
+./test/test_plugin.cmxa
./test/test_plugin.cmxs
./test/test.v
./test/test.vo
diff --git a/test-suite/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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 05:01:43 +0000