From 01603706ebf60b8c268a444fb645132acf448060 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 14 Dec 2000 01:41:11 +0000
Subject: MAJ

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

(limited to 'PROBLEMES')

diff --git a/PROBLEMES b/PROBLEMES
index c6cda0e7fc..08bd848fc2 100644
--- a/PROBLEMES
+++ b/PROBLEMES
@@ -12,7 +12,9 @@ MUTUAL-EXCLUSION/binary/version1/Soundness.v
 
 l'entree numarg de g_tactic.ml4 accepte aussi des id... (pour les
 binding je pense) d'ou des erreurs de syntaxe ...  pure_numarg est
-plus sūr
+plus sūr 
+REPONSE PROVISOIRE: si c'est pour Specialize, faudrait en changer la
+syntaxe, elle est incompatible avec L_tac.
 
 Associativite Repeat Orelse changee
 	Repeat A Orelse B se lit (Repeat A) Orelse B 
@@ -21,7 +23,8 @@ 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])
+Syntax error: 'as' or ',' or [ne_pattern_list] expected after
+[Constr.pattern] (in [compound_pattern])        ...CORRIGE
 
 CONTRIBS
 ---------
-- 
cgit v1.2.3