diff options
| author | Pierre Letouzey | 2014-03-01 19:50:59 +0100 |
|---|---|---|
| committer | Pierre Letouzey | 2014-03-02 20:00:02 +0100 |
| commit | 4b68dbe3428740a61cda825d3a45047571d9f299 (patch) | |
| tree | 487dff0e37d819e7de07196eac6f4699f8ab1f96 /pretyping/miscops.mli | |
| parent | 412f848e681e3c94c635f65638310a13d675449e (diff) | |
Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code
NB: new file miscprint.ml deserves to be part of printing.cma,
but should be part of proofs.cma for the moment, due to use in logic.ml
Diffstat (limited to 'pretyping/miscops.mli')
| -rw-r--r-- | pretyping/miscops.mli | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli index cf984113f6..84541a3b2a 100644 --- a/pretyping/miscops.mli +++ b/pretyping/miscops.mli @@ -13,12 +13,6 @@ open Misctypes val map_cast_type : ('a -> 'b) -> 'a cast_type -> 'b cast_type val smartmap_cast_type : ('a -> 'a) -> 'a cast_type -> 'a cast_type -(** Printing of [intro_pattern] *) +(** Equalities on [glob_sort] *) -val pr_intro_pattern : intro_pattern_expr Loc.located -> Pp.std_ppcmds -val pr_or_and_intro_pattern : or_and_intro_pattern_expr -> Pp.std_ppcmds - -(** Printing of [move_location] *) - -val pr_move_location : - ('a -> Pp.std_ppcmds) -> 'a move_location -> Pp.std_ppcmds +val glob_sort_eq : glob_sort -> glob_sort -> bool |