diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 2 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 5 | ||||
| -rw-r--r-- | parsing/prettyp.ml | 2 | ||||
| -rw-r--r-- | parsing/printer.ml | 6 |
4 files changed, 10 insertions, 5 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 7494ffd7c..2fd822636 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -538,6 +538,8 @@ GEXTEND Gram | IDENT "Existing"; IDENT "Instance"; is = identref -> VernacDeclareInstance is + | IDENT "Existing"; IDENT "Class"; is = identref -> VernacDeclareClass is + (* Implicit *) | IDENT "Implicit"; IDENT "Arguments"; qid = smart_global; pos = OPT [ "["; l = LIST0 implicit_name; "]" -> diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 8a8248bf4..6449add92 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -741,7 +741,10 @@ let rec pr_vernac = function | VernacDeclareInstance id -> - hov 1 (str"Instance" ++ spc () ++ pr_lident id) + hov 1 (str"Existing" ++ spc () ++ str"Instance" ++ spc () ++ pr_lident id) + + | VernacDeclareClass id -> + hov 1 (str"Existing" ++ spc () ++ str"Class" ++ spc () ++ pr_lident id) (* Modules and Module Types *) | VernacDefineModule (export,m,bl,ty,bd) -> diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index f96a94fb4..b7e218719 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -786,7 +786,7 @@ let print_typeclasses () = let pr_instance env i = (* gallina_print_constant_with_infos i.is_impl *) (* lighter *) - print_ref false (ConstRef (instance_impl i)) + print_ref false (instance_impl i) let print_all_instances () = let env = Global.env () in diff --git a/parsing/printer.ml b/parsing/printer.ml index eacad74c4..d9dced791 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -540,9 +540,9 @@ let cmap_to_list m = Cmap.fold (fun k v acc -> v :: acc) m [] open Typeclasses -let pr_instance i = - pr_global (ConstRef (instance_impl i)) - +let pr_instance i = + pr_global (instance_impl i) + let pr_instance_gmap insts = prlist_with_sep fnl (fun (gr, insts) -> prlist_with_sep fnl pr_instance (cmap_to_list insts)) |