From 64b269a68bf6dfb583ccbaf1f8a86cfd87530561 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 8 Sep 2001 08:24:02 +0000
Subject: MAJ

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

diff --git a/PROBLEMES b/PROBLEMES
index b392d8269f..4e522a8add 100644
--- a/PROBLEMES
+++ b/PROBLEMES
@@ -1,3 +1,16 @@
+Intuition plante en 7.1 à certains endroits où il réussissait en 6.3.
+Y a-t-il une explication ? (cf contrib sheaves de Chicli - HH)
+
+----------------------------------------------------------------------
+Theorem toto : (A:Prop)A->A.
+Refine [A;x]?.
+produit le message "type_of: this is not a well-typed term. Please report."
+
+----------------------------------------------------------------------
+"Intro until 1" plante avec le message 
+"Error: Internal tactic intro cannot be applied to intro until #GENTERM 1"
+--> intro est répété + GENTERM
+
 ----------------------------------------------------------------------
 La synthèse du ? dans l'exemple suivant se fait en V6 mais pas en V7:
 
-- 
cgit v1.2.3