MAJ

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1295 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 16 insertions, 7 deletions

diff --git a/.depend b/.depend
index bab209a8d7..281ecbe5e4 100644
--- a/.depend
+++ b/.depend
@@ -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 \
diff --git a/CHANGES b/CHANGES
index 34093e18d9..e87d107361 100644
--- a/CHANGES
+++ b/CHANGES
@@ -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
 
diff --git a/PROBLEMES b/PROBLEMES
index c1467caba3..43be1f5f40 100644
--- a/PROBLEMES
+++ b/PROBLEMES
@@ -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