numarg -> pure_numarg a poursuivre

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1084 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 33 insertions, 15 deletions

diff --git a/PROBLEMES b/PROBLEMES
index aed157912..ff4e7e582 100644
--- a/PROBLEMES
+++ b/PROBLEMES
@@ -9,14 +9,30 @@ l'application de la tactique, ils ne peuvent pas contenir des variables
 qui seront introduites dans la tactique ....
 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 sur
+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
 
 Associativite Repeat Orelse changee
 	Repeat A Orelse B se lit (Repeat A) Orelse B 
 ce n'est pas malin car Repeat A n'echoue jamais
 
+Probleme de Reset Initial.
+Load Field.
+Reset Initial.
+Coq <  Load Field.
+Error while reading ./Field.v :
+File "./Field.v", line 6, characters 0-83
+Error: list already exists
+(* l'erreur ne se produit pas sur un fichier plus court ..)
+voir dans library states.ml 
+la fonction freeze=set_state qui modifie l'etat initial ....
+
+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])
+
 CONTRIBS
 ---------
 BellLabs/lazyPCF : OK
@@ -42,10 +58,16 @@ Lyon/IEEE754 : OK
 Lyon/COINDUCTIVES : 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.
+/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
+Warning: Found several default clauses, kept the first one
+
+File "./cgraph.v", line 1866, characters 2-7
+Error: frontier was handed back a ill-formed proof.
+(Apres un EApply)
 
 Rocq/MUTUAL-EXCLUSION/
 	Incompatibilite interpretation des arguments de Tactic Definition
@@ -76,18 +98,14 @@ 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
 
+Rocq/DEMOS/Demo_AutoRewrite
+Anomaly: Invalid argument "output_value: functional value".
+
+
 Montevideo/CtlTctl OK
 Montevideo/RailroadCrossing
 File "./railroad_crossing.v", line 613, characters 2-20