diff options
| author |  mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-06 08:51:26 +0000 |
|---|---|---|
| committer | mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-06 08:51:26 +0000 |
| commit | 2c4473a7e52614b48292bee80fa903f416d05887 (patch) | |
| tree | b1ef159e787426579bb5d44579d45f1076eb6f84 /PROBLEMES | |
| parent | 908672c4eb9bba99c43e8bb2a7376656429af6d7 (diff) | |
Pour la phase debugage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1058 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'PROBLEMES')
| -rw-r--r-- | PROBLEMES | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/PROBLEMES b/PROBLEMES new file mode 100644 index 000000000..98282d5ee --- /dev/null +++ b/PROBLEMES @@ -0,0 +1,30 @@ +Declaration de Local a l'interieur d'un but ... +add_entry etait fait avant cache_object qui peut echouer en laissant +la lib_stk dans un etat incoherent .... + + +CONTRIBS +--------- +BellLabs/lazyPCF/OpSem/ +File "./utils.v", line 231, characters 14-18 +Syntax error: [Tactic.constrarg_binding_list] expected after [Tactic.numarg] (in [Tactic.simple_tactic]) +Specialize A2 with ... + +Bordeaux/TREES : +File "./ABR.v", line 131, characters 0-88 +Anomaly: Unrecognizable ast node of vernac arg: + (COMMAND (PROP {Null})). Please report. + +Derive Inversion_clear HAS_INV with + (n,p:nat)(t1,t2:bintree)(has (bin n t1 t2) p). + +Bordeaux/Additions : + echecs sur Realizer + +Bordeaux/GROUPS : 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.
\ No newline at end of file |