aboutsummaryrefslogtreecommitdiff
path: root/configure
diff options
context:
space:
mode:
authorfilliatr2000-12-15 14:26:58 +0000
committerfilliatr2000-12-15 14:26:58 +0000
commitd608222a594861efbae01e71018b8dcfc143e09a (patch)
treedbcd4e2ac871b95c15471de3939873bc3684b7e7 /configure
parent7872cda8545ba82827d34e6940b83f5809990f9d (diff)
- suppression mind_extract_params
- contraintes univers parametres inductifs prises en compte - exception UniverseInconsistency donne un message "Error: Universe Inconsistency" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1125 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure2
1 files changed, 1 insertions, 1 deletions
diff --git a/configure b/configure
index de53019b72..191a9f13c1 100755
--- a/configure
+++ b/configure
@@ -6,7 +6,7 @@
#
##################################
-VERSION=7.00
+VERSION=7.0
VERSIONSI=1.0
DATE="November 2000"