diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-15 16:07:11 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-15 16:07:11 +0000 |
| commit | 10451b08825aa6430bda2698755a81f6c9cfb056 (patch) | |
| tree | 99b2a53a1f8bd2fdbcf512498f0def5c7a2aa279 /PROBLEMES | |
| parent | d608222a594861efbae01e71018b8dcfc143e09a (diff) | |
mise a jour
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1126 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'PROBLEMES')
| -rw-r--r-- | PROBLEMES | 6 |
1 files changed, 2 insertions, 4 deletions
@@ -45,7 +45,6 @@ Lyon/COINDUCTIVES : OK Rocq/GRAPHS /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 @@ -70,9 +69,8 @@ Refine --> PROBLEME RESOLU MAIS LE MESSAGE D'ERREUR RESTE PAS TRES CLAIR Rocq/PARADOXES -File "./BuraliForti.v", line 176, characters 0-26 -Anomaly: Uncaught exception Univ.UniverseInconsistency. Please report. -A la fermeture de section, est-ce normal ? pourquoi une anomalie ? +File "./Reynolds1.v", line 105, characters 0-429 +Error: checking of theorem per_F0 failed... aborting Rocq/CHECKER OK Rocq/COMPILER OK |