From 0d294b3c91e0b93cb71d3b4ef1f00ef06ad711a6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 25 Dec 2000 18:59:08 +0000
Subject: MAJ

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1207 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ANNONCE     |  6 +++---
 CHANGEMENTS |  6 +++++-
 PROBLEMES   | 25 +++++--------------------
 3 files changed, 13 insertions(+), 24 deletions(-)

diff --git a/ANNONCE b/ANNONCE
index 81d2671400..30eca7f390 100644
--- a/ANNONCE
+++ b/ANNONCE
@@ -10,9 +10,9 @@ provided for users willing to experiment the new features which are:
   - an improved Search facilities using patterns (by Yves Bertot)
   - a "natural" syntax for real numbers (by Micaëla Mayero)
   - various bug fixes
-  - a command to export definitions, theorems and proofs to XML to be used with
-    Helm's publishing and rendering tools (see http://www.cs.unibo.it/helm)
-    (by Claudio Sacerdoti Coen)
+  - a command to export theories to XML to be used with Helm's publishing
+    and rendering tools (see http://www.cs.unibo.it/helm) (by Claudio
+    Sacerdoti Coen)
 
   Extraction and the Realizer/Program tactics are not available in Coq
 V7.0beta.
diff --git a/CHANGEMENTS b/CHANGEMENTS
index c2fd34ffaf..8f45a25a21 100644
--- a/CHANGEMENTS
+++ b/CHANGEMENTS
@@ -28,7 +28,8 @@ Extensions de syntaxe avec Grammar et Syntax
 
 - L'analyseur syntaxique considère maintenant comme token toute suite
   de symboles (source d'incompatibilité : il faut insérer des espaces
-  entre tokens spéciaux consécutifs).
+  entre tokens spéciaux consécutifs). Les tokens contenant non
+  constitués de caractères spéciaux sont provisoirement interdits.
 
 - L'entrée "command" dans "Grammar" et dans les piquants s'appelle
   maintenant "constr" comme dans "Syntax".
@@ -63,6 +64,9 @@ Syntaxe des constructions
 - Cases engendre parfois des noms differents (source théorique
   d'incompatibilité mais insensible dans la pratique)
 
+- Les alias de motifs ayant un type dépendant ne sont pour l'instant
+  pas traités
+
 - Davantage d'inférence automatique de "?".
 
 - Davantage d'arguments implicites engendrés par le discharge.
diff --git a/PROBLEMES b/PROBLEMES
index 427b524db9..5cdbfbfc24 100644
--- a/PROBLEMES
+++ b/PROBLEMES
@@ -24,20 +24,11 @@ Bordeaux/EXCEPTIONS : OK
 Dyade/Otway-Rees : OK
 Dyade/BDD : 
 File "./bdd4.v", line 122, characters 10-28
-Error: Tactic generated a subgoal identical to the original goal.
+--> Out of memory après plus de 500Mo utilisés
 
 Lyon/AUTOMATA : OK
 Lyon/CIRCUITS : OK
-Lyon/COINDUCTIVES : 
-File "./Specified_Streams.v", line 11, characters 0-132
-Error: Illegal application (Type Error): 
-The term SStream of type (A:Set)(nat->A->Prop)->Set
-cannot be applied to the terms
- A : Set
- x : (SStream A P)
-The 2nd term has type (SStream A P) which should be coercible to
- nat->A->Prop
-
+Lyon/COINDUCTIVES : OK
 Lyon/IEEE754 : OK
 
 Rocq/MUTUAL-EXCLUSION : échec sur Realizer
@@ -47,8 +38,8 @@ Realizer dans Conv_Dec.v, Expr.v, Infer.v, Machine.v MyList.v Names.v
 File "./Int_typ.v", line 209, characters 30-44
 Problème d'alias dépendant dans un Cases (idem SUBST)
 
-Rocq/ALGEBRA/RELATIONS/Relations.v
---> Un problème de Coercion au discharge
+Rocq/ALGEBRA/SETOIDS
+--> Token "=_S" non reconnus
 
 Rocq/ARITH/Chinese
 File "./Zdiv.v", line 34, characters 0-944
@@ -88,10 +79,4 @@ Montevideo/RailroadCrossing OK (TemporalOperators.v ne doit pas etre compile)
 
 Nijmegen OK
 Utrecht/Ramsey OK
-
-Utrecht/ABP
-coqc  -q  -I . abp_base
-File "./abp_base.v", line 42, characters 0-154
-Error: Cannot declare a variable or hypothesis over the term Y
-because this term is not a type.
---> Pb de calcul de de Bruijn dans le vieux Match
+Utrecht/ABP OK
-- 
cgit v1.2.3