From f0a72e4ad15038e1ef6b62195864db3efef80af0 Mon Sep 17 00:00:00 2001
From: mohring
Date: Wed, 6 Dec 2000 10:07:54 +0000
Subject: *** empty log message ***

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

diff --git a/PROBLEMES b/PROBLEMES
index f5068ba9f5..d9f10d7622 100644
--- a/PROBLEMES
+++ b/PROBLEMES
@@ -48,3 +48,31 @@ 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 ?
 
+Rocq/CHECKER OK
+Rocq/COMPILER OK
+Rocq/DEMOS OK
+Rocq/HIGMAN OK
+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
+
+Rocq/RATIONAL
+	Rewrite/LeibnizRewrite
+/home/cpaulin/coq/V7/bin/coqc  -q -byte -I . -I ../MLstuff HS
+[Loading ML file struct.cmo ...done]
+[Loading ML file sort_tac.cmo ...failed]
+File "./HS.v", line 6, characters 0-30
+Error: Cannot link ml-object sort_tac.cmo to Coq code.
+
+Rocq/SUBST
+File "./TS.v", line 69, characters 0-6
+Error: Attempt to save an incomplete proof
+
+Montevideo/CtlTctl OK
+Montevideo/RailroadCrossing
+File "./railroad_crossing.v", line 613, characters 2-20
+Anomaly: useInversionLemma. Please report.
-- 
cgit v1.2.3