diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-02-12 11:20:58 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-02-12 11:20:58 +0000 |
| commit | bd1e31d0e3f20e82778306bd27e0b0f8cd475757 (patch) | |
| tree | 81e275d60779c253f197b217cba3b965f1cdab11 /parsing | |
| parent | 21b5fa26bb25b07b38d96f0b4d3c144b923d0269 (diff) | |
Ajout Print Canonical Structures
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6711 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_basevernac.ml4 | 1 | ||||
| -rw-r--r-- | parsing/g_vernacnew.ml4 | 1 | ||||
| -rw-r--r-- | parsing/prettyp.ml | 14 | ||||
| -rw-r--r-- | parsing/prettyp.mli | 1 |
4 files changed, 13 insertions, 4 deletions
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index 79b0e26fc..a8f46a12b 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -191,6 +191,7 @@ GEXTEND Gram | IDENT "Coercions" -> PrintCoercions | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr -> PrintCoercionPaths (s,t) + | IDENT "Canonical"; IDENT "Structures" -> PrintCanonicalStructures | IDENT "Tables" -> PrintTables | "Proof"; qid = global -> PrintOpaqueName qid | IDENT "Hint" -> PrintHintGoal diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4 index e920352d1..5b0350f82 100644 --- a/parsing/g_vernacnew.ml4 +++ b/parsing/g_vernacnew.ml4 @@ -579,6 +579,7 @@ GEXTEND Gram | IDENT "Coercions" -> PrintCoercions | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr -> PrintCoercionPaths (s,t) + | IDENT "Canonical"; IDENT "Structures" -> PrintCanonicalStructures | IDENT "Tables" -> PrintTables (* Obsolete: was used for cooking V6.3 recipes ?? | IDENT "Proof"; qid = global -> PrintOpaqueName qid diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index bbbbc3180..50347df03 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -27,6 +27,7 @@ open Printer open Printmod open Libnames open Nametab +open Recordops (*********************) (** Basic printing *) @@ -593,10 +594,10 @@ let print_class i = pr_class cl let print_path ((i,j),p) = - (str"[" ++ - prlist_with_sep pr_semicolon print_coercion_value p ++ - str"] : " ++ print_class i ++ str" >-> " ++ - print_class j) + hov 2 ( + str"[" ++ hov 0 (prlist_with_sep pr_semicolon print_coercion_value p) ++ + str"] : ") ++ + print_class i ++ str" >-> " ++ print_class j let _ = Classops.install_path_printer print_path @@ -627,4 +628,9 @@ let print_path_between cls clt = in print_path ((i,j),p) +let print_canonical_structures () = + prlist_with_sep pr_fnl (fun ((r1,r2),o) -> + prterm o.o_DEF ++ str ": " ++ pr_global r1 ++ str " >-> " ++ pr_global r2) + (canonical_structures ()) + (*************************************************************************) diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli index 3af935d08..20429cd3d 100644 --- a/parsing/prettyp.mli +++ b/parsing/prettyp.mli @@ -57,6 +57,7 @@ val print_graph : unit -> std_ppcmds val print_classes : unit -> std_ppcmds val print_coercions : unit -> std_ppcmds val print_path_between : Classops.cl_typ -> Classops.cl_typ -> std_ppcmds +val print_canonical_structures : unit -> std_ppcmds val inspect : int -> std_ppcmds |