From 2c4473a7e52614b48292bee80fa903f416d05887 Mon Sep 17 00:00:00 2001
From: mohring
Date: Wed, 6 Dec 2000 08:51:26 +0000
Subject: Pour la phase debugage

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

diff --git a/PROBLEMES b/PROBLEMES
new file mode 100644
index 0000000000..98282d5ee3
--- /dev/null
+++ b/PROBLEMES
@@ -0,0 +1,30 @@
+Declaration de Local a l'interieur d'un but ...
+add_entry etait fait avant cache_object qui peut echouer en laissant 
+la lib_stk dans un etat incoherent ....
+
+
+CONTRIBS
+---------
+BellLabs/lazyPCF/OpSem/
+File "./utils.v", line 231, characters 14-18
+Syntax error: [Tactic.constrarg_binding_list] expected after [Tactic.numarg] (in [Tactic.simple_tactic])
+Specialize A2 with ...
+
+Bordeaux/TREES :
+File "./ABR.v", line 131, characters 0-88
+Anomaly: Unrecognizable ast node of vernac arg:
+ (COMMAND (PROP {Null})). Please report.
+
+Derive Inversion_clear HAS_INV with 
+    (n,p:nat)(t1,t2:bintree)(has (bin n t1 t2) p).
+
+Bordeaux/Additions : 
+	echecs sur Realizer
+
+Bordeaux/GROUPS : OK
+
+Rocq/GRAPHS
+File "./lsort.v", line 82, characters 4-17
+Error: Impossible to unify ad with
+ (a:ad)(?334 a)->(?334 (ad_double_plus_un a))
+Induction a.
\ No newline at end of file
-- 
cgit v1.2.3