diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-15 09:50:23 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-15 09:50:23 +0000 |
| commit | ac594661da831e91f8c5a1b118ce13b90a7ec85f (patch) | |
| tree | 5e05a326463d463968ccd6df89c0bd1d9981dd15 /kernel | |
| parent | 125f04f251e62674379dfe9ae7ee660586e5c954 (diff) | |
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
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/univ.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index a127fd5c0..dd00a5428 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. |