diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-07-13 19:53:54 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-07-19 16:00:30 +0200 |
commit | 9051c1618062ce014719de5c3f73832e9a282a4d (patch) | |
tree | 9197008d190e21f99dbaf08967d57f8ebd43c8ce /printing | |
parent | e273ff57ef82e81ab6b6309584a7d496ae4659c1 (diff) |
[general] Move files to directories matching linking order.
We move a bunch of modules (`Impargs`, `Declare`, `Ind_tables`,
`Miscprint`) to their proper place as they were declared in different
`mllib` files than the one in their directory.
In some cases this could be refined but we don't do anything fancy, we
just reflect the status quo.
Diffstat (limited to 'printing')
-rw-r--r-- | printing/miscprint.ml | 74 | ||||
-rw-r--r-- | printing/miscprint.mli | 37 |
2 files changed, 0 insertions, 111 deletions
diff --git a/printing/miscprint.ml b/printing/miscprint.ml deleted file mode 100644 index 5d37c8a02..000000000 --- a/printing/miscprint.ml +++ /dev/null @@ -1,74 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Misctypes -open Pp - -(** Printing of [intro_pattern] *) - -let rec pr_intro_pattern prc (_,pat) = match pat with - | IntroForthcoming true -> str "*" - | IntroForthcoming false -> str "**" - | IntroNaming p -> pr_intro_pattern_naming p - | IntroAction p -> pr_intro_pattern_action prc p - -and pr_intro_pattern_naming = function - | IntroIdentifier id -> Nameops.pr_id id - | IntroFresh id -> str "?" ++ Nameops.pr_id id - | IntroAnonymous -> str "?" - -and pr_intro_pattern_action prc = function - | IntroWildcard -> str "_" - | IntroOrAndPattern pll -> pr_or_and_intro_pattern prc pll - | IntroInjection pl -> - str "[=" ++ hv 0 (prlist_with_sep spc (pr_intro_pattern prc) pl) ++ - str "]" - | IntroApplyOn ((_,c),pat) -> pr_intro_pattern prc pat ++ str "%" ++ prc c - | IntroRewrite true -> str "->" - | IntroRewrite false -> str "<-" - -and pr_or_and_intro_pattern prc = function - | IntroAndPattern pl -> - str "(" ++ hv 0 (prlist_with_sep pr_comma (pr_intro_pattern prc) pl) ++ str ")" - | IntroOrPattern pll -> - str "[" ++ - hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc (pr_intro_pattern prc)) pll) - ++ str "]" - -(** Printing of [move_location] *) - -let pr_move_location pr_id = function - | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id - | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id - | MoveFirst -> str " at top" - | MoveLast -> str " at bottom" - -(** Printing of bindings *) -let pr_binding prc = function - | loc, (NamedHyp id, c) -> hov 1 (Names.Id.print id ++ str " := " ++ cut () ++ prc c) - | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) - -let pr_bindings prc prlc = function - | ImplicitBindings l -> - brk (1,1) ++ str "with" ++ brk (1,1) ++ - pr_sequence prc l - | ExplicitBindings l -> - brk (1,1) ++ str "with" ++ brk (1,1) ++ - pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l - | NoBindings -> mt () - -let pr_bindings_no_with prc prlc = function - | ImplicitBindings l -> - brk (0,1) ++ prlist_with_sep spc prc l - | ExplicitBindings l -> - brk (0,1) ++ prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l - | NoBindings -> mt () - -let pr_with_bindings prc prlc (c,bl) = - hov 1 (prc c ++ pr_bindings prc prlc bl) - diff --git a/printing/miscprint.mli b/printing/miscprint.mli deleted file mode 100644 index 21d410c7b..000000000 --- a/printing/miscprint.mli +++ /dev/null @@ -1,37 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Misctypes - -(** Printing of [intro_pattern] *) - -val pr_intro_pattern : - ('a -> Pp.std_ppcmds) -> 'a intro_pattern_expr Loc.located -> Pp.std_ppcmds - -val pr_or_and_intro_pattern : - ('a -> Pp.std_ppcmds) -> 'a or_and_intro_pattern_expr -> Pp.std_ppcmds - -val pr_intro_pattern_naming : intro_pattern_naming_expr -> Pp.std_ppcmds - -(** Printing of [move_location] *) - -val pr_move_location : - ('a -> Pp.std_ppcmds) -> 'a move_location -> Pp.std_ppcmds - -val pr_bindings : - ('a -> Pp.std_ppcmds) -> - ('a -> Pp.std_ppcmds) -> 'a bindings -> Pp.std_ppcmds - -val pr_bindings_no_with : - ('a -> Pp.std_ppcmds) -> - ('a -> Pp.std_ppcmds) -> 'a bindings -> Pp.std_ppcmds - -val pr_with_bindings : - ('a -> Pp.std_ppcmds) -> - ('a -> Pp.std_ppcmds) -> 'a * 'a bindings -> Pp.std_ppcmds - |