Correction du problème de complexité de Print Assumptions :

- Suite à une modification faite maladroitement, on ne se contentait pas 
de comparer le nom de la supposition quand on l'insérait dans l'ensemble 
des suppositions utilisées, mais aussi son type, ce qui était 
inutilement long (mais pas le facteur principal)
- L'environnement était parcouru deux fois pour chaque variable de 
section. Ce n'était pas très grave vu qu'en général on a assez peu de 
variables de sections sous la main. Mais ça restait inutile.
- Les noms qui ont déjà étés explorés sont maintenant memoizés, ce qui 
gagne dans le cas les pires (comme les théorèmes sur les réels 
typiquement) une exponentiel dans le temps de recherche (si on visualise 
l'espace de recherche comme un DAG, l'ancienne procédure le parcourais 
comme si il était un arbre, ce qui a une complexité exponentielle en la 
taille du DAG). 



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

1 files changed, 1 insertions, 1 deletions

diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index ba40ffd87..b3a985b63 100644
--- a/theories/Numbers/Cyclic/Int31/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
@@ -43,7 +43,7 @@ Inductive int31 : Type := I31 : nfun digits size int31.
 
 (* spiwack: Registration of the type of integers, so that the matchs in
    the functions below perform dynamic decompilation (otherwise some segfault
-   occur when they are applied to one non-closed term and one closed term *)
+   occur when they are applied to one non-closed term and one closed term). *)
 Register digits as int31 bits in "coq_int31" by True.
 Register int31 as int31 type in "coq_int31" by True.