diff options
| author |  delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-19 16:57:11 +0000 |
|---|---|---|
| committer | delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-19 16:57:11 +0000 |
| commit | 92b8ea381bfae4344602b3c9ab3036e1b5db8d01 (patch) | |
| tree | 5825c63f95096ad0b635333057ef9bb36426b718 /PROBLEMES | |
| parent | b41a1cd0edd2fc4a0da2a04f10554a4737a5c192 (diff) | |
DEMOS passe et MUTUAL-EXCLUSION aussi modulo Realizer
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1157 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'PROBLEMES')
| -rw-r--r-- | PROBLEMES | 31 |
1 files changed, 4 insertions, 27 deletions
@@ -1,31 +1,9 @@ -AddPath "/toto". -Anomaly: Uncaught exception Unix.Unix_error(20, "stat", "/toto"). -Please report. ---> CORRIGE - 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 <A>x=y est parfois refusee -Les arguments des Tactic Definition sont interpretes avant -l'application de la tactique, ils ne peuvent pas contenir des variables -qui seront introduites dans la tactique .... -MUTUAL-EXCLUSION/binary/version1/Soundness.v - ---> Il y a aussi une anomalie : -fntf1 < (SolveCycleNode1 H '(not_true_is_false (hd o))). -Toplevel input, characters 0-47 -> (SolveCycleNode1 H '(not_true_is_false (hd o))). - -> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Anomaly: Illegal application: (APP SolveCycleNode1 H - (COMMAND - (APPLIST (QUALID not_true_is_false) - (APPLIST (QUALID hd) (QUALID o))))). - - 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 @@ -37,8 +15,8 @@ CONTRIBS BellLabs/lazyPCF : OK Bordeaux/TREES : -Bordeaux/Additions : - echecs sur Realizer +Bordeaux/Additions : + echecs sur Realizer Bordeaux/GROUPS : OK @@ -74,7 +52,7 @@ The 2nd term has type (SStream A P) which should be coercible to Lyon/IEEE754 : OK - +Rocq/DEMOS : OK Rocq/GRAPHS /home/cpaulin/TYPES/V7/bin/coqc -q -I . lsort Utilise NewInduction @@ -86,8 +64,7 @@ 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 +Rocq/MUTUAL-EXCLUSION : échec sur Realizer Rocq/COC Realizer dans Conv_Dec.v, Expr.v, Infer.v, Machine.v MyList.v Names.v |