From 10451b08825aa6430bda2698755a81f6c9cfb056 Mon Sep 17 00:00:00 2001
From: filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 15 Dec 2000 16:07:11 +0000
Subject: mise a jour

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

diff --git a/PROBLEMES b/PROBLEMES
index bf3bfb06a..40bc23f48 100644
--- a/PROBLEMES
+++ b/PROBLEMES
@@ -45,7 +45,6 @@ Lyon/COINDUCTIVES : OK
 
 Rocq/GRAPHS
 /home/cpaulin/TYPES/V7/bin/coqc  -q  -I . lsort
-Warning: compute_metamap: MV(1506) sans type !
 Utilise NewInduction
 
 /home/cpaulin/TYPES/V7/bin/coqc  -q  -I . cgraph
@@ -70,9 +69,8 @@ Refine
 --> PROBLEME RESOLU MAIS LE MESSAGE D'ERREUR RESTE PAS TRES CLAIR
 
 Rocq/PARADOXES
-File "./BuraliForti.v", line 176, characters 0-26
-Anomaly: Uncaught exception Univ.UniverseInconsistency. Please report.
-A la fermeture de section, est-ce normal ? pourquoi une anomalie ?
+File "./Reynolds1.v", line 105, characters 0-429
+Error: checking of theorem per_F0 failed... aborting
 
 Rocq/CHECKER OK
 Rocq/COMPILER OK
-- 
cgit v1.2.3