From ac594661da831e91f8c5a1b118ce13b90a7ec85f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 15 Mar 2008 09:50:23 +0000
Subject: Application de refresh_universes dans typing.ml et retyping.ml : les
 appels à type_of et get_type_of sont souvent utilisés pour construire des
 termes à partir de types; on ne rajoute pas non plus de contraintes inutiles
 parce que type_of et get_type_of ne changent pas le graphe de contraintes;
 tout ce qu'on perd est une information utilisateur sur le type en lui-même
 mais puisque pretty.ml n'appelle ni type_of ni get_type_of, ces informations
 sur la représentation interne des univers restent a priori accessibles pour
 l'utilisateur.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10674 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/univ.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index a127fd5c09..dd00a54284 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -79,7 +79,7 @@ let super = function
   | Atom u -> 
       Max ([],[u])
   | Max _ ->
-      anomaly ("Cannot take the successor of a non variable universes:\n"^
+      anomaly ("Cannot take the successor of a non variable universe:\n"^
                "(maybe a bugged tactic)")
 
 (* Returns the formal universe that is greater than the universes u and v.
-- 
cgit v1.2.3