diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-02-19 10:43:17 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-02-19 10:43:17 +0000 |
| commit | 62c6c0ccc1930a556eeeab9b7a2050929cd790f1 (patch) | |
| tree | c8cbcdd3efef5706f0a60f280da4942b55124b5e /checker/indtypes.ml | |
| parent | 2383b30bb6efd01f68547113ac5019fb53b44479 (diff) | |
[checker] fixed vo validation problems, module incompatibilities remain
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12799 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker/indtypes.ml')
| -rw-r--r-- | checker/indtypes.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/checker/indtypes.ml b/checker/indtypes.ml index e0aa9e7c3..de57c50a7 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -22,7 +22,7 @@ open Environ let rec debug_string_of_mp = function | MPfile sl -> string_of_dirpath sl | MPbound uid -> "bound("^string_of_mbid uid^")" - | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l + | MPdot (mp,l) -> debug_string_of_mp mp ^ "." ^ string_of_label l let rec string_of_mp = function | MPfile sl -> string_of_dirpath sl @@ -36,8 +36,9 @@ let prkn kn = let (mp,_,l) = repr_kn kn in str(string_of_mp mp ^ "." ^ string_of_label l) let prcon c = - let (mp,_,l) = repr_con c in - str(string_of_mp mp ^ "." ^ string_of_label l) + let ck = canonical_con c in + let uk = user_con c in + if ck=uk then prkn uk else (prkn uk ++str"(="++prkn ck++str")") (* Same as noccur_between but may perform reductions. Could be refined more... *) |