aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/ppconstr.ml22
-rw-r--r--printing/ppconstr.mli5
-rw-r--r--printing/pputils.ml3
-rw-r--r--printing/pputils.mli3
-rw-r--r--printing/prettyp.ml9
-rw-r--r--printing/prettyp.mli7
6 files changed, 22 insertions, 27 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index e877b3c63d..6057819931 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -15,15 +15,15 @@ open Pp
open CAst
open Names
open Nameops
-open Constr
open Libnames
open Pputils
open Ppextend
-open Notation_gram
+open Glob_term
open Constrexpr
open Constrexpr_ops
+open Notation_gram
open Decl_kinds
-open Misctypes
+open Namegen
(*i*)
module Tag =
@@ -228,7 +228,7 @@ let tag_var = tag Tag.variable
str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")"
let pr_opt_type_spc pr = function
- | { CAst.v = CHole (_,Misctypes.IntroAnonymous,_) } -> mt ()
+ | { CAst.v = CHole (_,IntroAnonymous,_) } -> mt ()
| t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t
let pr_lident {loc; v=id} =
@@ -242,8 +242,8 @@ let tag_var = tag Tag.variable
| x -> pr_ast Name.print x
let pr_or_var pr = function
- | ArgArg x -> pr x
- | ArgVar id -> pr_lident id
+ | Locus.ArgArg x -> pr x
+ | Locus.ArgVar id -> pr_lident id
let pr_prim_token = function
| Numeral (n,s) -> str (if s then n else "-"^n)
@@ -363,7 +363,7 @@ let tag_var = tag Tag.variable
end
| Default b ->
match t with
- | { CAst.v = CHole (_,Misctypes.IntroAnonymous,_) } ->
+ | { CAst.v = CHole (_,IntroAnonymous,_) } ->
let s = prlist_with_sep spc pr_lname nal in
hov 1 (surround_implicit b s)
| _ ->
@@ -457,7 +457,7 @@ let tag_var = tag Tag.variable
let pr_case_type pr po =
match po with
- | None | Some { CAst.v = CHole (_,Misctypes.IntroAnonymous,_) } -> mt()
+ | None | Some { CAst.v = CHole (_,IntroAnonymous,_) } -> mt()
| Some p ->
spc() ++ hov 2 (keyword "return" ++ pr_sep_com spc (pr lsimpleconstr) p)
@@ -592,7 +592,7 @@ let tag_var = tag Tag.variable
hv 0 (str"{|" ++ pr_record_body_gen (pr spc) l ++ str" |}"),
latom
)
- | CCases (LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[{v=([[p]],b)}]) ->
+ | CCases (Constr.LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[{v=([[p]],b)}]) ->
return (
hv 0 (
keyword "let" ++ spc () ++ str"'" ++
@@ -643,9 +643,9 @@ let tag_var = tag Tag.variable
lif
)
- | CHole (_,Misctypes.IntroIdentifier id,_) ->
+ | CHole (_,IntroIdentifier id,_) ->
return (str "?[" ++ pr_id id ++ str "]", latom)
- | CHole (_,Misctypes.IntroFresh id,_) ->
+ | CHole (_,IntroFresh id,_) ->
return (str "?[?" ++ pr_id id ++ str "]", latom)
| CHole (_,_,_) ->
return (str "_", latom)
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 05f48ec79d..ce37c3614a 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -15,14 +15,13 @@
open Libnames
open Constrexpr
open Names
-open Misctypes
open Notation_gram
val prec_less : precedence -> tolerability -> bool
val pr_tight_coma : unit -> Pp.t
-val pr_or_var : ('a -> Pp.t) -> 'a or_var -> Pp.t
+val pr_or_var : ('a -> Pp.t) -> 'a Locus.or_var -> Pp.t
val pr_lident : lident -> Pp.t
val pr_lname : lname -> Pp.t
@@ -39,7 +38,7 @@ val pr_name : Name.t -> Pp.t
[@@ocaml.deprecated "alias of Names.Name.print"]
val pr_qualid : qualid -> Pp.t
-val pr_patvar : patvar -> Pp.t
+val pr_patvar : Pattern.patvar -> Pp.t
val pr_glob_level : Glob_term.glob_level -> Pp.t
val pr_glob_sort : Glob_term.glob_sort -> Pp.t
diff --git a/printing/pputils.ml b/printing/pputils.ml
index c14aa318e1..c6b8d50222 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -11,7 +11,6 @@
open Util
open Pp
open Genarg
-open Misctypes
open Locus
open Genredexpr
@@ -122,7 +121,7 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) keyword = function
let pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_ref,pr_pattern) =
pr_red_expr (pr_constr env sigma, pr_lconstr env sigma, pr_ref, pr_pattern env sigma)
-let pr_or_by_notation f = function
+let pr_or_by_notation f = let open Constrexpr in function
| {CAst.loc; v=AN v} -> f v
| {CAst.loc; v=ByNotation (s,sc)} -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
diff --git a/printing/pputils.mli b/printing/pputils.mli
index 6039168f88..5b1969e232 100644
--- a/printing/pputils.mli
+++ b/printing/pputils.mli
@@ -9,7 +9,6 @@
(************************************************************************)
open Genarg
-open Misctypes
open Locus
open Genredexpr
@@ -18,7 +17,7 @@ val pr_ast : ('a -> Pp.t) -> 'a CAst.t -> Pp.t
(** Prints an object surrounded by its commented location *)
val pr_or_var : ('a -> Pp.t) -> 'a or_var -> Pp.t
-val pr_or_by_notation : ('a -> Pp.t) -> 'a or_by_notation -> Pp.t
+val pr_or_by_notation : ('a -> Pp.t) -> 'a Constrexpr.or_by_notation -> Pp.t
val pr_with_occurrences :
('a -> Pp.t) -> (string -> Pp.t) -> 'a with_occurrences -> Pp.t
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 895181bc51..fe6cf73c79 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 *)
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 50042d6c5b..0375cfc921 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -12,7 +12,6 @@ open Names
open Environ
open Reductionops
open Libnames
-open Misctypes
open Evd
(** A Pretty-Printer for the Calculus of Inductive Constructions. *)
@@ -33,12 +32,12 @@ val print_eval :
reduction_function -> env -> Evd.evar_map ->
Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t
-val print_name : env -> Evd.evar_map -> reference or_by_notation ->
+val print_name : env -> Evd.evar_map -> reference Constrexpr.or_by_notation ->
UnivNames.univ_name_list option -> Pp.t
val print_opaque_name : env -> Evd.evar_map -> reference -> Pp.t
-val print_about : env -> Evd.evar_map -> reference or_by_notation ->
+val print_about : env -> Evd.evar_map -> reference Constrexpr.or_by_notation ->
UnivNames.univ_name_list option -> Pp.t
-val print_impargs : reference or_by_notation -> Pp.t
+val print_impargs : reference Constrexpr.or_by_notation -> Pp.t
(** Pretty-printing functions for classes and coercions *)
val print_graph : env -> evar_map -> Pp.t
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 07:35:42 +0000