diff options
| author | barras | 2008-09-02 15:10:46 +0000 |
|---|---|---|
| committer | barras | 2008-09-02 15:10:46 +0000 |
| commit | c1de637b6c9f5d074e534bf75cf5e407d95be7ff (patch) | |
| tree | 9b0823538dfab109a2efce1e5876163eb4896837 /checker/indtypes.ml | |
| parent | 3e314a8811fbc94d46247da9969432d94ed5eff0 (diff) | |
fixed bug #1927 + univ constraints (module cstrs include cstrs of its subcomponents)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11348 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker/indtypes.ml')
| -rw-r--r-- | checker/indtypes.ml | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 8c84fb0fa1..4c9b3d61db 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -19,6 +19,21 @@ open Pp open Declarations open Environ +let rec debug_string_of_mp = function + | MPfile sl -> string_of_dirpath sl + | MPbound uid -> "bound("^string_of_mbid uid^")" + | MPself uid -> "self("^string_of_msid uid^")" + | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l + +let rec string_of_mp = function + | MPfile sl -> string_of_dirpath sl + | MPbound uid -> string_of_mbid uid + | MPself uid -> string_of_msid uid + | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l + +let string_of_mp mp = + if !Flags.debug then debug_string_of_mp mp else string_of_mp mp + let prkn kn = let (mp,_,l) = repr_kn kn in str(string_of_mp mp ^ "." ^ string_of_label l) |