diff options
| -rw-r--r-- | .depend | 14 | ||||
| -rw-r--r-- | CHANGES | 5 | ||||
| -rw-r--r-- | PROBLEMES | 4 |
3 files changed, 16 insertions, 7 deletions
@@ -1084,17 +1084,19 @@ toplevel/discharge.cmo: toplevel/class.cmi pretyping/classops.cmi \ kernel/environ.cmi library/global.cmi library/impargs.cmi \ kernel/inductive.cmi kernel/instantiate.cmi library/lib.cmi \ library/libobject.cmi library/library.cmi kernel/names.cmi \ - library/nametab.cmi lib/options.cmi lib/pp.cmi pretyping/recordops.cmi \ - kernel/reduction.cmi kernel/sign.cmi library/summary.cmi kernel/term.cmi \ - kernel/typeops.cmi lib/util.cmi toplevel/discharge.cmi + library/nametab.cmi lib/options.cmi lib/pp.cmi toplevel/recordobj.cmi \ + pretyping/recordops.cmi kernel/reduction.cmi kernel/sign.cmi \ + library/summary.cmi kernel/term.cmi kernel/typeops.cmi lib/util.cmi \ + toplevel/discharge.cmi toplevel/discharge.cmx: toplevel/class.cmx pretyping/classops.cmx \ kernel/cooking.cmx kernel/declarations.cmx library/declare.cmx \ kernel/environ.cmx library/global.cmx library/impargs.cmx \ kernel/inductive.cmx kernel/instantiate.cmx library/lib.cmx \ library/libobject.cmx library/library.cmx kernel/names.cmx \ - library/nametab.cmx lib/options.cmx lib/pp.cmx pretyping/recordops.cmx \ - kernel/reduction.cmx kernel/sign.cmx library/summary.cmx kernel/term.cmx \ - kernel/typeops.cmx lib/util.cmx toplevel/discharge.cmi + library/nametab.cmx lib/options.cmx lib/pp.cmx toplevel/recordobj.cmx \ + pretyping/recordops.cmx kernel/reduction.cmx kernel/sign.cmx \ + library/summary.cmx kernel/term.cmx kernel/typeops.cmx lib/util.cmx \ + toplevel/discharge.cmi toplevel/errors.cmo: parsing/ast.cmi toplevel/himsg.cmi kernel/indtypes.cmi \ parsing/lexer.cmi proofs/logic.cmi lib/options.cmi lib/pp.cmi \ proofs/tacmach.cmi kernel/type_errors.cmi kernel/univ.cmi lib/util.cmi \ @@ -7,6 +7,11 @@ Différences V7.0beta / V7.0 - Rétablissement des @Definition and co - Rétablissement des token extensibles et mélangeant symboles et lettres +Différences oubliées dans la V7.0beta : + +- Du fait des noms qualifiés, les variables de buts n'évitent plus les +globaux de même nom de base + ---------------------------------------------------------------------- English version of changes is available on @@ -1,4 +1,5 @@ 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 *) @@ -60,7 +61,8 @@ File "./Int_typ.v", line 209, characters 30-44 Problème d'alias dépendant dans un Cases (idem SUBST) Rocq/ALGEBRA/SETOIDS ---> Token "=_S" non reconnus +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 |