From 34fcbe510f105ed241d443fef941ba47eae041e6 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Fri, 30 Mar 2001 12:35:44 +0000
Subject: repertoire pour les tests d'extraction

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1504 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/extraction/test/.cvsignore | 1 +
 contrib/extraction/test/bench      | 6 ++++++
 contrib/extraction/test/bench.v    | 7 +++++++
 3 files changed, 14 insertions(+)
 create mode 100644 contrib/extraction/test/.cvsignore
 create mode 100755 contrib/extraction/test/bench
 create mode 100644 contrib/extraction/test/bench.v

diff --git a/contrib/extraction/test/.cvsignore b/contrib/extraction/test/.cvsignore
new file mode 100644
index 0000000000..7166b260b6
--- /dev/null
+++ b/contrib/extraction/test/.cvsignore
@@ -0,0 +1 @@
+*.ml
diff --git a/contrib/extraction/test/bench b/contrib/extraction/test/bench
new file mode 100755
index 0000000000..8b29f5f155
--- /dev/null
+++ b/contrib/extraction/test/bench
@@ -0,0 +1,6 @@
+#!/bin/sh
+../../../bin/coqtop.byte -batch -load-vernac-source ../Extraction.v -load-vernac-source ./bench.v
+ocamlc -c -i polylist.ml
+ocamlc -c -i zarith.ml
+ocamlc -c -i even.ml
+
diff --git a/contrib/extraction/test/bench.v b/contrib/extraction/test/bench.v
new file mode 100644
index 0000000000..84eed5e877
--- /dev/null
+++ b/contrib/extraction/test/bench.v
@@ -0,0 +1,7 @@
+Require PolyList.
+Extraction "polylist.ml" nth nth_in_or_default.
+Require ZArith.
+Extraction "zarith.ml" Zmult.
+Require Even.
+Extraction "even.ml" even_odd_dec.
+
-- 
cgit v1.2.3