diff options
| author | herbelin | 2001-02-05 23:06:33 +0000 |
|---|---|---|
| committer | herbelin | 2001-02-05 23:06:33 +0000 |
| commit | 9759a74e3910ba12608f7bcddd40f7d97247dbcc (patch) | |
| tree | e473ca4d9858ba1316212d17217540e61e7b6ba4 /parsing/pretty.ml | |
| parent | c9aa1b6d908d3a4f8d9906ba0f11c0bb11569ab7 (diff) | |
Restructuration de classops; évolution en une version mieux intégrée au reste du système; conséquences collatérales
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1327 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/pretty.ml')
| -rw-r--r-- | parsing/pretty.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/parsing/pretty.ml b/parsing/pretty.ml index d7d0926851..eb6b207192 100644 --- a/parsing/pretty.ml +++ b/parsing/pretty.ml @@ -439,7 +439,7 @@ let string_of_strength = function | NeverDischarge -> "(global)" | DischargeAt sp -> "(disch@"^(string_of_dirpath sp) -let print_coercion_value v = prterm v.cOE_VALUE.uj_val +let print_coercion_value v = prterm (get_coercion_value v) let print_index_coercion c = let _,v = coercion_info_from_index c in @@ -465,7 +465,7 @@ let print_classes () = [< prlist_with_sep pr_spc (fun (_,(cl,x)) -> [< 'sTR (string_of_class cl) - (*; 'sTR(string_of_strength x.cL_STRE) *) >]) + (*; 'sTR(string_of_strength x.cl_strength) *) >]) (classes()) >] let print_coercions () = @@ -483,7 +483,7 @@ let cl_of_id id = let index_cl_of_id id = try let cl = cl_of_id id in - let i,_=class_info cl in + let i,_ = class_info cl in i with _ -> errorlabstrm "index_cl_of_id" |