diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-06-20 13:52:21 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-06-20 13:52:21 +0000 |
| commit | 6314b34d1eb8d8614706068020566d776f0a50fb (patch) | |
| tree | fff299ea7ce4c6538e457a413202051a1ace2ee0 /contrib/subtac/test | |
| parent | cc68954e80969fbc73b60c1ce6e4ad4ed553ccd7 (diff) | |
Rewrite of the recursive defs handling in progress.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8964 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/subtac/test')
| -rw-r--r-- | contrib/subtac/test/euclid.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/subtac/test/euclid.v b/contrib/subtac/test/euclid.v index 481b6708d..ba5bdf232 100644 --- a/contrib/subtac/test/euclid.v +++ b/contrib/subtac/test/euclid.v @@ -12,8 +12,8 @@ reflexivity. Defined. Extraction testsig. -Extraction sigS. -Extract Inductive sigS => "" [ "" ]. +Extraction sig. +Extract Inductive sig => "" [ "" ]. Extraction testsig. Require Import Coq.Arith.Compare_dec. |