diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-13 15:56:49 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-13 15:56:49 +0000 |
| commit | a8dddac7d3c13a902da81b1521dedc245f485243 (patch) | |
| tree | e269637c3008c74b8d791362fedd988852dcbc77 /contrib/extraction/test | |
| parent | 8a89173127428a02a30ed8ffa9b8083ef0ce757a (diff) | |
eliminiation des singletons du genre sig + divers
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1587 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/test')
| -rwxr-xr-x | contrib/extraction/test/bench | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/extraction/test/bench b/contrib/extraction/test/bench index 8b29f5f15..bff9bd77a 100755 --- a/contrib/extraction/test/bench +++ b/contrib/extraction/test/bench @@ -1,5 +1,5 @@ #!/bin/sh -../../../bin/coqtop.byte -batch -load-vernac-source ../Extraction.v -load-vernac-source ./bench.v +../../../bin/coqtop.byte -batch -load-vernac-source ./bench.v ocamlc -c -i polylist.ml ocamlc -c -i zarith.ml ocamlc -c -i even.ml |