diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-01 02:37:15 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-12 14:42:28 +0200 |
| commit | 615290d0f9d5cad7c508d45cf4ab89aecff033b2 (patch) | |
| tree | f5db022987df54435d807017f4f647ca9e275e9c /printing/prettyp.ml | |
| parent | 4aaeb5d429227505adfde9fe04c3c0fb69f2d37f (diff) | |
[api] Remove Misctypes.
We move the last 3 types to more adequate places.
Diffstat (limited to 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 895181bc5..fe6cf73c7 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -26,7 +26,6 @@ open Libobject open Libnames open Globnames open Recordops -open Misctypes open Printer open Printmod open Context.Rel.Declaration @@ -843,12 +842,12 @@ let print_any_name env sigma na udecl = let print_name env sigma na udecl = match na with - | {loc; v=ByNotation (ntn,sc)} -> + | {loc; v=Constrexpr.ByNotation (ntn,sc)} -> print_any_name env sigma (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)) udecl - | {loc; v=AN ref} -> + | {loc; v=Constrexpr.AN ref} -> print_any_name env sigma (locate_any_name ref) udecl let print_opaque_name env sigma qid = @@ -896,11 +895,11 @@ let print_about_any ?loc env sigma k udecl = let print_about env sigma na udecl = match na with - | {loc;v=ByNotation (ntn,sc)} -> + | {loc;v=Constrexpr.ByNotation (ntn,sc)} -> print_about_any ?loc env sigma (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)) udecl - | {loc;v=AN ref} -> + | {loc;v=Constrexpr.AN ref} -> print_about_any ?loc env sigma (locate_any_name ref) udecl (* for debug *) |