From 819d32734f187773af15100c35639b2a3858f8fe Mon Sep 17 00:00:00 2001
From: mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 15 Dec 2000 08:26:18 +0000
Subject: Mise a jour

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1118 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 PROBLEMES | 14 ++++----------
 1 file changed, 4 insertions(+), 10 deletions(-)

(limited to 'PROBLEMES')

diff --git a/PROBLEMES b/PROBLEMES
index d7d4c2fb6..ebd6c6b0d 100644
--- a/PROBLEMES
+++ b/PROBLEMES
@@ -24,12 +24,6 @@ Associativite Repeat Orelse changee
 	Repeat A Orelse B se lit (Repeat A) Orelse B 
 ce n'est pas malin car Repeat A n'echoue jamais
 
-les parentheses ne sont pas autorises autour de 
-motifs constants :
-> Check [n:nat]Cases n of (O) => true | _ => false end.
-Syntax error: 'as' or ',' or [ne_pattern_list] expected after
-[Constr.pattern] (in [compound_pattern])        ...CORRIGE
-
 CONTRIBS
 ---------
 BellLabs/lazyPCF : OK
@@ -88,10 +82,10 @@ Rocq/LAMBDA OK
 Rocq/SHUFFLE OK
 
 Rocq/SCHROEDER
-File "./Functions.v", line 95, characters 0-15
-Error: Bad inductive definition.
-A la fermeture de section
---> RESOLU Mais pb de "Remark" local à un thm pas pris en compte dans
+File "./Schroeder.v", line 351, characters 4-52
+Anomaly: type_of: variable h1 unbound. Please report.
+
+--> Pb de "Remark" local à un thm pas pris en compte dans
 l'environnement de la preuve de ce théorème
 
 Rocq/SUBST
-- 
cgit v1.2.3