Des CASTEDCOMMAND s'affiche dans les scripts de preuves.
Probleme d'affichage des scripts de preuve (disparition des THEN)
Compute affiche Cbv Beta Iota
Variable + Record => clash. Exemple:
======================================================================
Section S.
Variable F:Set.
Record R [ F:Set; x:F ] : Set := { c : x=x }.
=> Error: new_isevar_sign: two vars have the same name
======================================================================
Hints Resolve fait une anomalie si la constante n'existe pas
--> CORRIGÉ
(* Probleme de lancement de coqtop lorsque le fichier n'est pas sauve
sous emacs et qu'un lien (lock ?) .#fichier a ete cree *)
/home/cpaulin/coq/V7/bin/coqc -q -I . Axioms
Anomaly: Uncaught exception Unix.Unix_error(20, "stat", "/home/cpaulin/coq/V7/theories/Num/.#Axioms.v").
Please report.
make: *** [Axioms.vo] Error 1
--> CORRIGÉ (message explicatif et n'échoue plus)
Declaration de Local a l'interieur d'un but ...
Certains Clear deviennent impossible car la variable apparait dans
un lemme local, c'est plutot sain ...
La syntaxe x=y est parfois refusee
---> N'était-ce pas quand elle était précédée d'un symbole, style ~x=y ??
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
REPONSE PROVISOIRE: si c'est pour Specialize, faudrait en changer la
syntaxe, elle est incompatible avec L_tac.
CONTRIBS
---------
BellLabs/lazyPCF : OK
Bordeaux/Additions : échec sur Realizer
Bordeaux/SearchTrees : échec sur Realizer
Bordeaux/TREES : échec sur Realizer
Bordeaux/GROUPS : OK
Bordeaux/EXCEPTIONS : OK
Dyade/Otway-Rees : OK
Dyade/BDD :
File "./bdd4.v", line 122, characters 10-28
<<<<<<< PROBLEMES
Error: Tactic generated a subgoal identical to the original goal.
Lannion : échec sur Realizer
Lyon/AUTOMATA : OK
Lyon/CIRCUITS : OK
Lyon/COINDUCTIVES : OK
Lyon/IEEE754 : OK
Rocq/MUTUAL-EXCLUSION : échec sur Realizer
Rocq/ALGEBRA/SETOIDS
File "CATEGORY_THEORY/CATEGORY/ONE.v", line 83, characters 0-61
Error: There is an unknown subterm I cannot solve
Rocq/ARITH/Chinese
File "./Zdiv.v", line 34, characters 0-944
--> Un Refine mal typé et des Realizer
Rocq/COC
Realizer dans Conv_Dec.v, Expr.v, Infer.v, Machine.v MyList.v Names.v
File "./Int_typ.v", line 209, characters 30-44
Problème d'alias dépendant dans un Cases (idem SUBST)
Rocq/DEMOS OK
Rocq/GRAPHS OK
Rocq/LAMBDA OK
Rocq/SHUFFLE OK
Rocq/THREE_GAP OK
Rocq/ZF OK
Rocq/PARADOXES OK
Rocq/CHECKER OK
Rocq/COMPILER OK
Rocq/HIGMAN OK
Rocq/SUBST
File "./inversionSL.v", line 215, characters 38-39
Problème d'alias dépendant dans un Cases
Rocq/SCHROEDER
File "./Schroeder.v", line 351, characters 4-52
Anomaly: type_of: variable h1 unbound. Please report.
--> Pb de "Remark" local à un thm pas pris en compte dans
l'environnement de la preuve de ce théorème
Rocq/TreeAutomata: Un Rewrite ou Unfold en a trop ou pas assez fait (union.v)
Rocq/RATIONAL
--> Des fichiers ML à porter
Lyon/AUTOMATA OK
Lyon/CIRCUITS OK
Lyon/COINDUCTIVES OK
Lyon/IEEE754 (passait dans la V7.0beta !!)
File "./IEEE754_def.v", line 427, characters 0-1194
Error: Some clauses are redondant
Lyon/PROCESSES OK
Lyon/PROGRAMS : Nécessite Programs.v
Lyon/STREAMS OK
Lyon/FIRING-SQUAD : des identificateurs avec le symbole $ !! (plus autorisé)
Lyon/INSERTION-SORT : Nécessite Programs.v
Lyon/DISTRIBUTED_REFERENCE_COUNTING
File "./fifo.v", line 181, characters 0-6
Error: Attempt to save an incomplete proof
--> Preuve incomplète (lié à Intuition)
Marseille/CCS OK
Marseille/CIRCUITS -> Realizer
Montevideo/CtlTctl OK
Montevideo/RailroadCrossing OK (TemporalOperators.v ne doit pas etre compile)
Nancy/FOUnify OK
Nijmegen OK
Paris/ZF OK
Sophia-Antipolis/HARDWARE OK
Sophia-Antipolis/Cours-de-Coq OK
Sophia-Antipolis/MATHS/GEOMETRY
File "./part3.v", line 78, characters 0-5
Error: Attempt to save an incomplete proof
--> Changement de sémantique de Intuition
Sophia-Antipolis/condom ... vide
Sophia-Antipolis/param_pi
File "./fresh.v", line 173, characters 0-20
Error: Too few occurences
Suresnes/BDD OK
Utrecht/Ramsey OK
Utrecht/ABP OK