diff options
author | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-26 17:22:36 +0000 |
---|---|---|
committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-26 17:22:36 +0000 |
commit | 57eec1e1e4efd09f5181297d87b1908c284e6951 (patch) | |
tree | 043c9810a48393013b774f7335129b83c56c6bc4 /test-suite/bugs/closed/shouldsucceed/1414.v | |
parent | c9398a44487f406e03179ecedd768698adcb1903 (diff) |
Diverses petites modifs dans la test-suite:
test-suite/output/ZSyntax.out
typo
test-suite/bugs/closed/shouldsucceed/1776.v
bug closed
test-suite/success/extraction.v
test-suite/success/extraction.v
test-suite/bugs/closed/shouldsucceed/846.v
backtrack sur le commit 10639
test-suite/bugs/closed/shouldsucceed/1322.v:
petites modifications suite aux changement de setoid_replace
test-suite/bugs/closed/shouldsucceed/1414.v:
petites modifications suite aux changement dans Program
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10723 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/1414.v')
-rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1414.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1414.v b/test-suite/bugs/closed/shouldsucceed/1414.v index 9c2686ceb..d3c008087 100644 --- a/test-suite/bugs/closed/shouldsucceed/1414.v +++ b/test-suite/bugs/closed/shouldsucceed/1414.v @@ -1,4 +1,4 @@ -Require Import ZArith Coq.Program.Utils. +Require Import ZArith Coq.Program.Wf Coq.Program.Utils. Parameter data:Set. |