aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/genprint.ml66
-rw-r--r--printing/genprint.mli20
-rw-r--r--printing/ppconstr.ml25
-rw-r--r--printing/pputils.ml13
-rw-r--r--printing/pputils.mli8
-rw-r--r--printing/ppvernac.ml83
-rw-r--r--printing/prettyp.ml239
-rw-r--r--printing/prettyp.mli44
-rw-r--r--printing/printer.ml61
-rw-r--r--printing/printer.mli36
-rw-r--r--printing/printmod.ml35
-rw-r--r--printing/printmod.mli4
12 files changed, 362 insertions, 272 deletions
diff --git a/printing/genprint.ml b/printing/genprint.ml
index 776a212b5c..37a94fe219 100644
--- a/printing/genprint.ml
+++ b/printing/genprint.ml
@@ -16,21 +16,27 @@ open Geninterp
(* Printing generic values *)
-type printer_with_level =
+type 'a with_level =
{ default_already_surrounded : Notation_term.tolerability;
default_ensure_surrounded : Notation_term.tolerability;
- printer : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t }
+ printer : 'a }
type printer_result =
| PrinterBasic of (unit -> Pp.t)
-| PrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t)
-| PrinterNeedsContextAndLevel of printer_with_level
+| PrinterNeedsLevel of (Notation_term.tolerability -> Pp.t) with_level
-type 'a printer = 'a -> Pp.t
+type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t
-type 'a top_printer = 'a -> printer_result
+type top_printer_result =
+| TopPrinterBasic of (unit -> Pp.t)
+| TopPrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t)
+| TopPrinterNeedsContextAndLevel of printer_fun_with_level with_level
-module ValMap = ValTMap (struct type 'a t = 'a -> printer_result end)
+type 'a printer = 'a -> printer_result
+
+type 'a top_printer = 'a -> top_printer_result
+
+module ValMap = ValTMap (struct type 'a t = 'a -> top_printer_result end)
let print0_val_map = ref ValMap.empty
@@ -48,32 +54,32 @@ let register_val_print0 s pr =
print0_val_map := ValMap.add s pr !print0_val_map
let combine_dont_needs pr_pair pr1 = function
- | PrinterBasic pr2 ->
- PrinterBasic (fun () -> pr_pair (pr1 ()) (pr2 ()))
- | PrinterNeedsContext pr2 ->
- PrinterNeedsContext (fun env sigma ->
+ | TopPrinterBasic pr2 ->
+ TopPrinterBasic (fun () -> pr_pair (pr1 ()) (pr2 ()))
+ | TopPrinterNeedsContext pr2 ->
+ TopPrinterNeedsContext (fun env sigma ->
pr_pair (pr1 ()) (pr2 env sigma))
- | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
- PrinterNeedsContext (fun env sigma ->
+ | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
+ TopPrinterNeedsContext (fun env sigma ->
pr_pair (pr1 ()) (printer env sigma default_ensure_surrounded))
let combine_needs pr_pair pr1 = function
- | PrinterBasic pr2 ->
- PrinterNeedsContext (fun env sigma -> pr_pair (pr1 env sigma) (pr2 ()))
- | PrinterNeedsContext pr2 ->
- PrinterNeedsContext (fun env sigma ->
+ | TopPrinterBasic pr2 ->
+ TopPrinterNeedsContext (fun env sigma -> pr_pair (pr1 env sigma) (pr2 ()))
+ | TopPrinterNeedsContext pr2 ->
+ TopPrinterNeedsContext (fun env sigma ->
pr_pair (pr1 env sigma) (pr2 env sigma))
- | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
- PrinterNeedsContext (fun env sigma ->
+ | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
+ TopPrinterNeedsContext (fun env sigma ->
pr_pair (pr1 env sigma) (printer env sigma default_ensure_surrounded))
let combine pr_pair pr1 v2 =
match pr1 with
- | PrinterBasic pr1 ->
+ | TopPrinterBasic pr1 ->
combine_dont_needs pr_pair pr1 (generic_val_print v2)
- | PrinterNeedsContext pr1 ->
+ | TopPrinterNeedsContext pr1 ->
combine_needs pr_pair pr1 (generic_val_print v2)
- | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
+ | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
combine_needs pr_pair (fun env sigma -> printer env sigma default_ensure_surrounded)
(generic_val_print v2)
@@ -81,14 +87,14 @@ let _ =
let pr_cons a b = Pp.(a ++ spc () ++ b) in
register_val_print0 Val.typ_list
(function
- | [] -> PrinterBasic mt
+ | [] -> TopPrinterBasic mt
| a::l ->
List.fold_left (combine pr_cons) (generic_val_print a) l)
let _ =
register_val_print0 Val.typ_opt
(function
- | None -> PrinterBasic Pp.mt
+ | None -> TopPrinterBasic Pp.mt
| Some v -> generic_val_print v)
let _ =
@@ -99,9 +105,9 @@ let _ =
(* Printing generic arguments *)
type ('raw, 'glb, 'top) genprinter = {
- raw : 'raw printer;
- glb : 'glb printer;
- top : 'top -> printer_result;
+ raw : 'raw -> printer_result;
+ glb : 'glb -> printer_result;
+ top : 'top -> top_printer_result;
}
module PrintObj =
@@ -112,9 +118,9 @@ struct
| ExtraArg tag ->
let name = ArgT.repr tag in
let printer = {
- raw = (fun _ -> str "<genarg:" ++ str name ++ str ">");
- glb = (fun _ -> str "<genarg:" ++ str name ++ str ">");
- top = (fun _ -> PrinterBasic (fun () -> str "<genarg:" ++ str name ++ str ">"));
+ raw = (fun _ -> PrinterBasic (fun () -> str "<genarg:" ++ str name ++ str ">"));
+ glb = (fun _ -> PrinterBasic (fun () -> str "<genarg:" ++ str name ++ str ">"));
+ top = (fun _ -> TopPrinterBasic (fun () -> str "<genarg:" ++ str name ++ str ">"));
} in
Some printer
| _ -> assert false
diff --git a/printing/genprint.mli b/printing/genprint.mli
index 2da9bbc36b..baa60fcb2e 100644
--- a/printing/genprint.mli
+++ b/printing/genprint.mli
@@ -10,19 +10,25 @@
open Genarg
-type printer_with_level =
+type 'a with_level =
{ default_already_surrounded : Notation_term.tolerability;
default_ensure_surrounded : Notation_term.tolerability;
- printer : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t }
+ printer : 'a }
type printer_result =
| PrinterBasic of (unit -> Pp.t)
-| PrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t)
-| PrinterNeedsContextAndLevel of printer_with_level
+| PrinterNeedsLevel of (Notation_term.tolerability -> Pp.t) with_level
-type 'a printer = 'a -> Pp.t
+type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t
-type 'a top_printer = 'a -> printer_result
+type top_printer_result =
+| TopPrinterBasic of (unit -> Pp.t)
+| TopPrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t)
+| TopPrinterNeedsContextAndLevel of printer_fun_with_level with_level
+
+type 'a printer = 'a -> printer_result
+
+type 'a top_printer = 'a -> top_printer_result
val raw_print : ('raw, 'glb, 'top) genarg_type -> 'raw printer
(** Printer for raw level generic arguments. *)
@@ -34,7 +40,7 @@ val top_print : ('raw, 'glb, 'top) genarg_type -> 'top top_printer
(** Printer for top level generic arguments. *)
val register_print0 : ('raw, 'glb, 'top) genarg_type ->
- 'raw printer -> 'glb printer -> ('top -> printer_result) -> unit
+ 'raw printer -> 'glb printer -> 'top top_printer -> unit
val register_val_print0 : 'top Geninterp.Val.typ ->
'top top_printer -> unit
val register_vernac_print0 : ('raw, 'glb, 'top) genarg_type ->
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 0f6452de69..2abbc389fa 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -150,10 +150,15 @@ let tag_var = tag Tag.variable
let pr_sep_com sep f c = pr_with_comments ?loc:(constr_loc c) (sep() ++ f c)
+ let pr_univ_expr = function
+ | Some (x,n) ->
+ pr_reference x ++ (match n with 0 -> mt () | _ -> str"+" ++ int n)
+ | None -> str"_"
+
let pr_univ l =
match l with
- | [_,x] -> Name.print x
- | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> Name.print (snd x)) l ++ str")"
+ | [x] -> pr_univ_expr x
+ | l -> str"max(" ++ prlist_with_sep (fun () -> str",") pr_univ_expr l ++ str")"
let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}"
@@ -166,8 +171,9 @@ let tag_var = tag Tag.variable
let pr_glob_level = function
| GProp -> tag_type (str "Prop")
| GSet -> tag_type (str "Set")
- | GType None -> tag_type (str "Type")
- | GType (Some (_, u)) -> tag_type (Name.print u)
+ | GType UUnknown -> tag_type (str "Type")
+ | GType UAnonymous -> tag_type (str "_")
+ | GType (UNamed u) -> tag_type (pr_reference u)
let pr_qualid sp =
let (sl, id) = repr_qualid sp in
@@ -192,8 +198,9 @@ let tag_var = tag Tag.variable
tag_type (str "Set")
| GType u ->
(match u with
- | Some (_,u) -> Name.print u
- | None -> tag_type (str "Type"))
+ | UNamed u -> pr_reference u
+ | UAnonymous -> tag_type (str "Type")
+ | UUnknown -> tag_type (str "_"))
let pr_universe_instance l =
pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_glob_sort_instance)) l
@@ -396,7 +403,7 @@ let tag_var = tag Tag.variable
extract_prod_binders c
| { loc; v = CProdN ([[_,Name id],bk,t],
{ v = CCases (LetPatternStyle,None, [{ v = CRef (Ident (_,id'),None)},None,None],[(_,([_,[p]],b))])} ) }
- when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) ->
+ when Id.equal id id' && not (Id.Set.mem id (free_vars_of_constr_expr b)) ->
let bl,c = extract_prod_binders b in
CLocalPattern (loc, (p,None)) :: bl, c
| { loc; v = CProdN ((nal,bk,t)::bl,c) } ->
@@ -412,7 +419,7 @@ let tag_var = tag Tag.variable
extract_lam_binders c
| CLambdaN ([[_,Name id],bk,t],
{ v = CCases (LetPatternStyle,None, [{ v = CRef (Ident (_,id'),None)},None,None],[(_,([_,[p]],b))])} )
- when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) ->
+ when Id.equal id id' && not (Id.Set.mem id (free_vars_of_constr_expr b)) ->
let bl,c = extract_lam_binders b in
CLocalPattern (ce.loc,(p,None)) :: bl, c
| CLambdaN ((nal,bk,t)::bl,c) ->
@@ -430,7 +437,7 @@ let tag_var = tag Tag.variable
let rename na na' t c =
match (na,na') with
| (_,Name id), (_,Name id') ->
- (na',t,Topconstr.replace_vars_constr_expr (Id.Map.singleton id id') c)
+ (na',t,replace_vars_constr_expr (Id.Map.singleton id id') c)
| (_,Name id), (_,Anonymous) -> (na,t,c)
| _ -> (na',t,c)
diff --git a/printing/pputils.ml b/printing/pputils.ml
index 3cc7a3e6b9..a544b47623 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -103,6 +103,9 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) keyword = function
| CbvNative o ->
keyword "native_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o
+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
| AN v -> f v
| ByNotation (_,(s,sc)) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
@@ -127,7 +130,10 @@ let rec pr_raw_generic env (GenArg (Rawwit wit, x)) =
let q = in_gen (rawwit wit2) q in
hov_if_not_empty 0 (pr_sequence (pr_raw_generic env) [p; q])
| ExtraArg s ->
- Genprint.generic_raw_print (in_gen (rawwit wit) x)
+ let open Genprint in
+ match generic_raw_print (in_gen (rawwit wit) x) with
+ | PrinterBasic pp -> pp ()
+ | PrinterNeedsLevel { default_ensure_surrounded; printer } -> printer default_ensure_surrounded
let rec pr_glb_generic env (GenArg (Glbwit wit, x)) =
@@ -149,4 +155,7 @@ let rec pr_glb_generic env (GenArg (Glbwit wit, x)) =
let ans = pr_sequence (pr_glb_generic env) [p; q] in
hov_if_not_empty 0 ans
| ExtraArg s ->
- Genprint.generic_glb_print (in_gen (glbwit wit) x)
+ let open Genprint in
+ match generic_glb_print (in_gen (glbwit wit) x) with
+ | PrinterBasic pp -> pp ()
+ | PrinterNeedsLevel { default_ensure_surrounded; printer } -> printer default_ensure_surrounded
diff --git a/printing/pputils.mli b/printing/pputils.mli
index 1f4fa1390d..f7f586b773 100644
--- a/printing/pputils.mli
+++ b/printing/pputils.mli
@@ -21,8 +21,16 @@ val pr_with_occurrences :
val pr_short_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t
val pr_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t
+
val pr_red_expr :
('a -> Pp.t) * ('a -> Pp.t) * ('b -> Pp.t) * ('c -> Pp.t) ->
+ (string -> Pp.t) -> ('a,'b,'c) red_expr_gen -> Pp.t
+
+val pr_red_expr_env : Environ.env -> Evd.evar_map ->
+ (Environ.env -> Evd.evar_map -> 'a -> Pp.t) *
+ (Environ.env -> Evd.evar_map -> 'a -> Pp.t) *
+ ('b -> Pp.t) *
+ (Environ.env -> Evd.evar_map -> 'c -> Pp.t) ->
(string -> Pp.t) ->
('a,'b,'c) red_expr_gen -> Pp.t
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 143f9ddcc5..46ef2ac031 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -41,6 +41,11 @@ open Decl_kinds
pr_glob_level l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++
pr_glob_level r
+ let pr_univ_name_list = function
+ | None -> mt ()
+ | Some l ->
+ str "@{" ++ prlist_with_sep spc pr_lname l ++ str"}"
+
let pr_univdecl_instance l extensible =
prlist_with_sep spc pr_lident l ++
(if extensible then str"+" else mt ())
@@ -319,23 +324,18 @@ open Decl_kinds
| SortClass -> keyword "Sortclass"
| RefClass qid -> pr_smart_global qid
- let pr_assumption_token many (l,a) =
- let l = match l with Some x -> x | None -> Decl_kinds.Global in
- match l, a with
- | (Discharge,Logical) ->
- keyword (if many then "Hypotheses" else "Hypothesis")
- | (Discharge,Definitional) ->
- keyword (if many then "Variables" else "Variable")
- | (Global,Logical) ->
+ let pr_assumption_token many discharge kind =
+ match discharge, kind with
+ | (NoDischarge,Logical) ->
keyword (if many then "Axioms" else "Axiom")
- | (Global,Definitional) ->
+ | (NoDischarge,Definitional) ->
keyword (if many then "Parameters" else "Parameter")
- | (Local, Logical) ->
- keyword (if many then "Local Axioms" else "Local Axiom")
- | (Local,Definitional) ->
- keyword (if many then "Local Parameters" else "Local Parameter")
- | (Global,Conjectural) -> str"Conjecture"
- | ((Discharge | Local),Conjectural) ->
+ | (NoDischarge,Conjectural) -> str"Conjecture"
+ | (DoDischarge,Logical) ->
+ keyword (if many then "Hypotheses" else "Hypothesis")
+ | (DoDischarge,Definitional) ->
+ keyword (if many then "Variables" else "Variable")
+ | (DoDischarge,Conjectural) ->
anomaly (Pp.str "Don't know how to beautify a local conjecture.")
let pr_params pr_c (xl,(c,t)) =
@@ -447,7 +447,7 @@ open Decl_kinds
| PrintGrammar ent ->
keyword "Print Grammar" ++ spc() ++ str ent
| PrintLoadPath dir ->
- keyword "Print LoadPath" ++ pr_opt pr_dirpath dir
+ keyword "Print LoadPath" ++ pr_opt DirPath.print dir
| PrintModules ->
keyword "Print Modules"
| PrintMLLoadPath ->
@@ -488,8 +488,8 @@ open Decl_kinds
else "Print Universes"
in
keyword cmd ++ pr_opt str fopt
- | PrintName qid ->
- keyword "Print" ++ spc() ++ pr_smart_global qid
+ | PrintName (qid,udecl) ->
+ keyword "Print" ++ spc() ++ pr_smart_global qid ++ pr_univ_name_list udecl
| PrintModuleType qid ->
keyword "Print Module Type" ++ spc() ++ pr_reference qid
| PrintModule qid ->
@@ -502,9 +502,9 @@ open Decl_kinds
keyword "Print Scope" ++ spc() ++ str s
| PrintVisibility s ->
keyword "Print Visibility" ++ pr_opt str s
- | PrintAbout (qid,gopt) ->
+ | PrintAbout (qid,l,gopt) ->
pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt
- ++ keyword "About" ++ spc() ++ pr_smart_global qid
+ ++ keyword "About" ++ spc() ++ pr_smart_global qid ++ pr_univ_name_list l
| PrintImplicit qid ->
keyword "Print Implicit" ++ spc() ++ pr_smart_global qid
(* spiwack: command printing all the axioms and section variables used in a
@@ -518,7 +518,7 @@ open Decl_kinds
in
keyword cmd ++ spc() ++ pr_smart_global qid
| PrintNamespace dp ->
- keyword "Print Namespace" ++ pr_dirpath dp
+ keyword "Print Namespace" ++ DirPath.print dp
| PrintStrategy None ->
keyword "Print Strategies"
| PrintStrategy (Some qid) ->
@@ -626,7 +626,7 @@ open Decl_kinds
return (keyword "Fail" ++ spc() ++ pr_vernac_body v)
(* Syntax *)
- | VernacOpenCloseScope (_,(opening,sc)) ->
+ | VernacOpenCloseScope (opening,sc) ->
return (
keyword (if opening then "Open " else "Close ") ++
keyword "Scope" ++ spc() ++ str sc
@@ -655,7 +655,7 @@ open Decl_kinds
++ spc() ++ pr_smart_global q
++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]"
)
- | VernacInfix (_,((_,s),mv),q,sn) -> (* A Verifier *)
+ | VernacInfix (((_,s),mv),q,sn) -> (* A Verifier *)
return (
hov 0 (hov 0 (keyword "Infix "
++ qs s ++ str " :=" ++ pr_constrarg q) ++
@@ -664,7 +664,7 @@ open Decl_kinds
| None -> mt()
| Some sc -> spc() ++ str":" ++ spc() ++ str sc))
)
- | VernacNotation (_,c,((_,s),l),opt) ->
+ | VernacNotation (c,((_,s),l),opt) ->
return (
hov 2 (keyword "Notation" ++ spc() ++ qs s ++
str " :=" ++ Flags.without_option Flags.beautify pr_constrarg c ++ pr_syntax_modifiers l ++
@@ -672,7 +672,7 @@ open Decl_kinds
| None -> mt()
| Some sc -> str" :" ++ spc() ++ str sc))
)
- | VernacSyntaxExtension (_, _,(s,l)) ->
+ | VernacSyntaxExtension (_, (s, l)) ->
return (
keyword "Reserved Notation" ++ spc() ++ pr_located qs s ++
pr_syntax_modifiers l
@@ -683,10 +683,9 @@ open Decl_kinds
)
(* Gallina *)
- | VernacDefinition (d,id,b) -> (* A verifier... *)
- let pr_def_token (l,dk) =
- let l = match l with Some x -> x | None -> Decl_kinds.Global in
- keyword (Kindops.string_of_definition_kind (l,false,dk))
+ | VernacDefinition ((discharge,kind),id,b) -> (* A verifier... *)
+ let pr_def_token dk =
+ keyword (Kindops.string_of_definition_object_kind dk)
in
let pr_reduce = function
| None -> mt()
@@ -707,7 +706,7 @@ open Decl_kinds
let (binds,typ,c) = pr_def_body b in
return (
hov 2 (
- pr_def_token d ++ spc()
+ pr_def_token kind ++ spc()
++ pr_ident_decl id ++ binds ++ typ
++ (match c with
| None -> mt()
@@ -732,13 +731,13 @@ open Decl_kinds
)
| VernacExactProof c ->
return (hov 2 (keyword "Proof" ++ pr_lconstrarg c))
- | VernacAssumption (stre,t,l) ->
+ | VernacAssumption ((discharge,kind),t,l) ->
let n = List.length (List.flatten (List.map fst (List.map snd l))) in
let pr_params (c, (xl, t)) =
hov 2 (prlist_with_sep sep pr_ident_decl xl ++ spc() ++
(if c then str":>" else str":" ++ spc() ++ pr_lconstr_expr t)) in
let assumptions = prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params p ++ str ")")) l in
- return (hov 2 (pr_assumption_token (n > 1) stre ++
+ return (hov 2 (pr_assumption_token (n > 1) discharge kind ++
pr_non_empty_arg pr_assumption_inline t ++ spc() ++ assumptions))
| VernacInductive (cum, p,f,l) ->
let pr_constructor (coe,(id,c)) =
@@ -788,9 +787,8 @@ open Decl_kinds
| VernacFixpoint (local, recs) ->
let local = match local with
- | Some Discharge -> "Let "
- | Some Local -> "Local "
- | None | Some Global -> ""
+ | DoDischarge -> "Let "
+ | NoDischarge -> ""
in
return (
hov 0 (str local ++ keyword "Fixpoint" ++ spc () ++
@@ -800,9 +798,8 @@ open Decl_kinds
| VernacCoFixpoint (local, corecs) ->
let local = match local with
- | Some Discharge -> keyword "Let" ++ spc ()
- | Some Local -> keyword "Local" ++ spc ()
- | None | Some Global -> str ""
+ | DoDischarge -> keyword "Let" ++ spc ()
+ | NoDischarge -> str ""
in
let pr_onecorec ((iddecl,bl,c,def),ntn) =
pr_ident_decl iddecl ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
@@ -863,14 +860,14 @@ open Decl_kinds
return (
keyword "Canonical Structure" ++ spc() ++ pr_smart_global q
)
- | VernacCoercion (_,id,c1,c2) ->
+ | VernacCoercion (id,c1,c2) ->
return (
hov 1 (
keyword "Coercion" ++ spc() ++
pr_smart_global id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++
spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2)
)
- | VernacIdentityCoercion (_,id,c1,c2) ->
+ | VernacIdentityCoercion (id,c1,c2) ->
return (
hov 1 (
keyword "Identity Coercion" ++ spc() ++ pr_lident id ++
@@ -964,7 +961,7 @@ open Decl_kinds
keyword "LoadPath" ++ spc() ++ qs s ++
(match d with
| None -> mt()
- | Some dir -> spc() ++ keyword "as" ++ spc() ++ pr_dirpath dir))
+ | Some dir -> spc() ++ keyword "as" ++ spc() ++ DirPath.print dir))
)
| VernacRemoveLoadPath s ->
return (keyword "Remove LoadPath" ++ qs s)
@@ -994,9 +991,9 @@ open Decl_kinds
prlist_with_sep spc (fun r -> pr_id (coerce_reference_to_id r)) ids ++
pr_opt_hintbases dbnames)
)
- | VernacHints (_, dbnames,h) ->
+ | VernacHints (dbnames,h) ->
return (pr_hints dbnames h pr_constr pr_constr_pattern_expr)
- | VernacSyntacticDefinition (id,(ids,c),_,compat) ->
+ | VernacSyntacticDefinition (id,(ids,c),compat) ->
return (
hov 2
(keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index acbd2d5d2f..1eb2c31c88 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -15,7 +15,6 @@ open CErrors
open Util
open Names
open Nameops
-open Term
open Termops
open Declarations
open Environ
@@ -33,15 +32,15 @@ open Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
type object_pr = {
- print_inductive : MutInd.t -> Pp.t;
- print_constant_with_infos : Constant.t -> Pp.t;
- print_section_variable : variable -> Pp.t;
- print_syntactic_def : KerName.t -> Pp.t;
+ print_inductive : MutInd.t -> Universes.univ_name_list option -> Pp.t;
+ print_constant_with_infos : Constant.t -> Universes.univ_name_list option -> Pp.t;
+ print_section_variable : env -> Evd.evar_map -> variable -> Pp.t;
+ print_syntactic_def : env -> KerName.t -> Pp.t;
print_module : bool -> ModPath.t -> Pp.t;
print_modtype : ModPath.t -> Pp.t;
- print_named_decl : Context.Named.Declaration.t -> Pp.t;
- print_library_entry : bool -> (object_name * Lib.node) -> Pp.t option;
- print_context : bool -> int option -> Lib.library_segment -> Pp.t;
+ print_named_decl : env -> Evd.evar_map -> Context.Named.Declaration.t -> Pp.t;
+ print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option;
+ print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t;
print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t;
print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t;
}
@@ -69,7 +68,7 @@ let int_or_no n = if Int.equal n 0 then str "no" else int n
let print_basename sp = pr_global (ConstRef sp)
-let print_ref reduce ref =
+let print_ref reduce ref udecl =
let typ, ctx = Global.type_of_global_in_context (Global.env ()) ref in
let typ = Vars.subst_instance_constr (Univ.AUContext.instance ctx) typ in
let typ = EConstr.of_constr typ in
@@ -82,7 +81,8 @@ let print_ref reduce ref =
let inst = Univ.AUContext.instance univs in
let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in
let env = Global.env () in
- let bl = Universes.universe_binders_of_global ref in
+ let bl = Universes.universe_binders_with_opt_names ref
+ (Array.to_list (Univ.Instance.to_array inst)) udecl in
let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in
let inst =
if Global.is_polymorphic ref then Printer.pr_universe_instance sigma univs
@@ -139,7 +139,7 @@ let print_renames_list prefix l =
let need_expansion impl ref =
let typ, _ = Global.type_of_global_in_context (Global.env ()) ref in
- let ctx = prod_assum typ in
+ let ctx = Term.prod_assum typ in
let nprods = List.count is_local_assum ctx in
not (List.is_empty impl) && List.length impl >= nprods &&
let _,lastimpl = List.chop nprods impl in
@@ -151,7 +151,7 @@ let print_impargs ref =
let has_impl = not (List.is_empty impl) in
(* Need to reduce since implicits are computed with products flattened *)
pr_infos_list
- ([ print_ref (need_expansion (select_impargs_size 0 impl) ref) ref;
+ ([ print_ref (need_expansion (select_impargs_size 0 impl) ref) ref None;
blankline ] @
(if has_impl then print_impargs_list (mt()) impl
else [str "No implicit arguments"]))
@@ -257,7 +257,7 @@ let print_name_infos ref =
if need_expansion (select_impargs_size 0 impls) ref then
(* Need to reduce since implicits are computed with products flattened *)
[str "Expanded type for implicit arguments";
- print_ref true ref; blankline]
+ print_ref true ref None; blankline]
else
[] in
print_polymorphism ref @
@@ -360,13 +360,13 @@ let pr_located_qualid = function
str "Notation" ++ spc () ++ pr_path (Nametab.path_of_syndef kn)
| Dir dir ->
let s,dir = match dir with
- | DirOpenModule (dir,_) -> "Open Module", dir
- | DirOpenModtype (dir,_) -> "Open Module Type", dir
- | DirOpenSection (dir,_) -> "Open Section", dir
- | DirModule (dir,_) -> "Module", dir
+ | DirOpenModule { obj_dir ; _ } -> "Open Module", obj_dir
+ | DirOpenModtype { obj_dir ; _ } -> "Open Module Type", obj_dir
+ | DirOpenSection { obj_dir ; _ } -> "Open Section", obj_dir
+ | DirModule { obj_dir ; _ } -> "Module", obj_dir
| DirClosedSection dir -> "Closed Section", dir
in
- str s ++ spc () ++ pr_dirpath dir
+ str s ++ spc () ++ DirPath.print dir
| ModuleType mp ->
str "Module Type" ++ spc () ++ pr_path (Nametab.path_of_modtype mp)
| Other (obj, info) -> info.name obj
@@ -410,7 +410,7 @@ let locate_term qid =
let locate_module qid =
let all = Nametab.locate_extended_all_dir qid in
let map dir = match dir with
- | DirModule (_, (mp, _)) -> Some (Dir dir, Nametab.shortest_qualid_of_module mp)
+ | DirModule { obj_mp ; _ } -> Some (Dir dir, Nametab.shortest_qualid_of_module obj_mp)
| DirOpenModule _ -> Some (Dir dir, qid)
| _ -> None
in
@@ -487,25 +487,25 @@ let gallina_print_typed_value_in_env env sigma (trm,typ) =
the pretty-print of a proposition (P:(nat->nat)->Prop)(P [u]u)
synthesizes the type nat of the abstraction on u *)
-let print_named_def name body typ =
- let pbody = pr_lconstr body in
- let ptyp = pr_ltype typ in
- let pbody = if isCast body then surround pbody else pbody in
+let print_named_def env sigma name body typ =
+ let pbody = pr_lconstr_env env sigma body in
+ let ptyp = pr_ltype_env env sigma typ in
+ let pbody = if Constr.isCast body then surround pbody else pbody in
(str "*** [" ++ str name ++ str " " ++
hov 0 (str ":=" ++ brk (1,2) ++ pbody ++ spc () ++
str ":" ++ brk (1,2) ++ ptyp) ++
str "]")
-let print_named_assum name typ =
- str "*** [" ++ str name ++ str " : " ++ pr_ltype typ ++ str "]"
+let print_named_assum env sigma name typ =
+ str "*** [" ++ str name ++ str " : " ++ pr_ltype_env env sigma typ ++ str "]"
-let gallina_print_named_decl =
+let gallina_print_named_decl env sigma =
let open Context.Named.Declaration in
function
| LocalAssum (id, typ) ->
- print_named_assum (Id.to_string id) typ
+ print_named_assum env sigma (Id.to_string id) typ
| LocalDef (id, body, typ) ->
- print_named_def (Id.to_string id) body typ
+ print_named_def env sigma (Id.to_string id) body typ
let assumptions_for_print lna =
List.fold_right (fun na env -> add_name na env) lna empty_names_context
@@ -513,22 +513,22 @@ let assumptions_for_print lna =
(*********************)
(* *)
-let gallina_print_inductive sp =
+let gallina_print_inductive sp udecl =
let env = Global.env() in
let mib = Environ.lookup_mind sp env in
let mipv = mib.mind_packets in
- pr_mutual_inductive_body env sp mib ++
+ pr_mutual_inductive_body env sp mib udecl ++
with_line_skip
(print_primitive_record mib.mind_finite mipv mib.mind_record @
print_inductive_renames sp mipv @
print_inductive_implicit_args sp mipv @
print_inductive_argument_scopes sp mipv)
-let print_named_decl id =
- gallina_print_named_decl (Global.lookup_named id) ++ fnl ()
+let print_named_decl env sigma id =
+ gallina_print_named_decl env sigma (Global.lookup_named id) ++ fnl ()
-let gallina_print_section_variable id =
- print_named_decl id ++
+let gallina_print_section_variable env sigma id =
+ print_named_decl env sigma id ++
with_line_skip (print_name_infos (VarRef id))
let print_body env evd = function
@@ -546,7 +546,7 @@ let print_instance sigma cb =
pr_universe_instance sigma univs
else mt()
-let print_constant with_values sep sp =
+let print_constant with_values sep sp udecl =
let cb = Global.lookup_constant sp in
let val_0 = Global.body_of_constant_body cb in
let typ =
@@ -556,31 +556,34 @@ let print_constant with_values sep sp =
let inst = Univ.AUContext.instance univs in
Vars.subst_instance_constr inst cb.const_type
in
- let univs =
+ let univs, ulist =
+ let open Entries in
+ let open Univ in
let otab = Global.opaque_tables () in
match cb.const_body with
| Undef _ | Def _ ->
begin
match cb.const_universes with
- | Monomorphic_const ctx -> ctx
+ | Monomorphic_const ctx -> Monomorphic_const_entry ctx, []
| Polymorphic_const ctx ->
- let inst = Univ.AUContext.instance ctx in
- Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx)
+ let inst = AUContext.instance ctx in
+ Polymorphic_const_entry (UContext.make (inst, AUContext.instantiate inst ctx)),
+ Array.to_list (Instance.to_array inst)
end
| OpaqueDef o ->
let body_uctxs = Opaqueproof.force_constraints otab o in
match cb.const_universes with
| Monomorphic_const ctx ->
- let uctxs = Univ.ContextSet.of_context ctx in
- Univ.ContextSet.to_context (Univ.ContextSet.union body_uctxs uctxs)
+ Monomorphic_const_entry (ContextSet.union body_uctxs ctx), []
| Polymorphic_const ctx ->
- assert(Univ.ContextSet.is_empty body_uctxs);
- let inst = Univ.AUContext.instance ctx in
- Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx)
+ assert(ContextSet.is_empty body_uctxs);
+ let inst = AUContext.instance ctx in
+ Polymorphic_const_entry (UContext.make (inst, AUContext.instantiate inst ctx)),
+ Array.to_list (Instance.to_array inst)
in
let ctx =
Evd.evar_universe_context_of_binders
- (Universes.universe_binders_of_global (ConstRef sp))
+ (Universes.universe_binders_with_opt_names (ConstRef sp) ulist udecl)
in
let env = Global.env () and sigma = Evd.from_ctx ctx in
let pr_ltype = pr_ltype_env env sigma in
@@ -590,18 +593,18 @@ let print_constant with_values sep sp =
str"*** [ " ++
print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++
str" ]" ++
- Printer.pr_universe_ctx sigma univs
+ Printer.pr_constant_universes sigma univs
| Some (c, ctx) ->
let c = Vars.subst_instance_constr (Univ.AUContext.instance ctx) c in
print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++
(if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++
- Printer.pr_universe_ctx sigma univs)
+ Printer.pr_constant_universes sigma univs)
-let gallina_print_constant_with_infos sp =
- print_constant true " = " sp ++
+let gallina_print_constant_with_infos sp udecl =
+ print_constant true " = " sp udecl ++
with_line_skip (print_name_infos (ConstRef sp))
-let gallina_print_syntactic_def kn =
+let gallina_print_syntactic_def env kn =
let qid = Nametab.shortest_qualid_of_syndef Id.Set.empty kn
and (vars,a) = Syntax_def.search_syntactic_definition kn in
let c = Notation_ops.glob_constr_of_notation_constr a in
@@ -612,20 +615,20 @@ let gallina_print_syntactic_def kn =
spc () ++ str ":=") ++
spc () ++
Constrextern.without_specific_symbols
- [Notation.SynDefRule kn] pr_glob_constr c)
+ [Notation.SynDefRule kn] (pr_glob_constr_env env) c)
-let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) =
+let gallina_print_leaf_entry env sigma with_values ((sp,kn as oname),lobj) =
let sep = if with_values then " = " else " : "
and tag = object_tag lobj in
match (oname,tag) with
| (_,"VARIABLE") ->
(* Outside sections, VARIABLES still exist but only with universes
constraints *)
- (try Some(print_named_decl (basename sp)) with Not_found -> None)
+ (try Some(print_named_decl env sigma (basename sp)) with Not_found -> None)
| (_,"CONSTANT") ->
- Some (print_constant with_values sep (Constant.make1 kn))
+ Some (print_constant with_values sep (Constant.make1 kn) None)
| (_,"INDUCTIVE") ->
- Some (gallina_print_inductive (MutInd.make1 kn))
+ Some (gallina_print_inductive (MutInd.make1 kn) None)
| (_,"MODULE") ->
let (mp,_,l) = KerName.repr kn in
Some (print_module with_values (MPdot (mp,l)))
@@ -637,26 +640,26 @@ let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) =
(* To deal with forgotten cases... *)
| (_,s) -> None
-let gallina_print_library_entry with_values ent =
+let gallina_print_library_entry env sigma with_values ent =
let pr_name (sp,_) = Id.print (basename sp) in
match ent with
| (oname,Lib.Leaf lobj) ->
- gallina_print_leaf_entry with_values (oname,lobj)
+ gallina_print_leaf_entry env sigma with_values (oname,lobj)
| (oname,Lib.OpenedSection (dir,_)) ->
Some (str " >>>>>>> Section " ++ pr_name oname)
| (oname,Lib.ClosedSection _) ->
Some (str " >>>>>>> Closed Section " ++ pr_name oname)
- | (_,Lib.CompilingLibrary (dir,_)) ->
- Some (str " >>>>>>> Library " ++ pr_dirpath dir)
+ | (_,Lib.CompilingLibrary { obj_dir; _ }) ->
+ Some (str " >>>>>>> Library " ++ DirPath.print obj_dir)
| (oname,Lib.OpenedModule _) ->
Some (str " >>>>>>> Module " ++ pr_name oname)
| (oname,Lib.ClosedModule _) ->
Some (str " >>>>>>> Closed Module " ++ pr_name oname)
-let gallina_print_context with_values =
+let gallina_print_context env sigma with_values =
let rec prec n = function
| h::rest when Option.is_empty n || Option.get n > 0 ->
- (match gallina_print_library_entry with_values h with
+ (match gallina_print_library_entry env sigma with_values h with
| None -> prec n rest
| Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ())
| _ -> mt ()
@@ -718,10 +721,10 @@ let print_safe_judgment env sigma j =
(*********************)
(* *)
-let print_full_context () = print_context true None (Lib.contents ())
-let print_full_context_typ () = print_context false None (Lib.contents ())
+let print_full_context env sigma = print_context env sigma true None (Lib.contents ())
+let print_full_context_typ env sigma = print_context env sigma false None (Lib.contents ())
-let print_full_pure_context () =
+let print_full_pure_context env sigma =
let rec prec = function
| ((_,kn),Lib.Leaf lobj)::rest ->
let pp = match object_tag lobj with
@@ -733,20 +736,20 @@ let print_full_pure_context () =
match cb.const_body with
| Undef _ ->
str "Parameter " ++
- print_basename con ++ str " : " ++ cut () ++ pr_ltype typ
+ print_basename con ++ str " : " ++ cut () ++ pr_ltype_env env sigma typ
| OpaqueDef lc ->
str "Theorem " ++ print_basename con ++ cut () ++
- str " : " ++ pr_ltype typ ++ str "." ++ fnl () ++
- str "Proof " ++ pr_lconstr (Opaqueproof.force_proof (Global.opaque_tables ()) lc)
+ str " : " ++ pr_ltype_env env sigma typ ++ str "." ++ fnl () ++
+ str "Proof " ++ pr_lconstr_env env sigma (Opaqueproof.force_proof (Global.opaque_tables ()) lc)
| Def c ->
str "Definition " ++ print_basename con ++ cut () ++
- str " : " ++ pr_ltype typ ++ cut () ++ str " := " ++
- pr_lconstr (Mod_subst.force_constr c))
+ str " : " ++ pr_ltype_env env sigma typ ++ cut () ++ str " := " ++
+ pr_lconstr_env env sigma (Mod_subst.force_constr c))
++ str "." ++ fnl () ++ fnl ()
| "INDUCTIVE" ->
let mind = Global.mind_of_delta_kn kn in
let mib = Global.lookup_mind mind in
- pr_mutual_inductive_body (Global.env()) mind mib ++
+ pr_mutual_inductive_body (Global.env()) mind mib None ++
str "." ++ fnl () ++ fnl ()
| "MODULE" ->
(* TODO: make it reparsable *)
@@ -776,8 +779,8 @@ let read_sec_context r =
with Not_found ->
user_err ?loc ~hdr:"read_sec_context" (str "Unknown section.") in
let rec get_cxt in_cxt = function
- | (_,Lib.OpenedSection ((dir',_),_) as hd)::rest ->
- if DirPath.equal dir dir' then (hd::in_cxt) else get_cxt (hd::in_cxt) rest
+ | (_,Lib.OpenedSection ({obj_dir;_},_) as hd)::rest ->
+ if DirPath.equal dir obj_dir then (hd::in_cxt) else get_cxt (hd::in_cxt) rest
| (_,Lib.ClosedSection _)::rest ->
user_err Pp.(str "Cannot print the contents of a closed section.")
(* LEM: Actually, we could if we wanted to. *)
@@ -787,19 +790,28 @@ let read_sec_context r =
let cxt = Lib.contents () in
List.rev (get_cxt [] cxt)
-let print_sec_context sec =
- print_context true None (read_sec_context sec)
-
-let print_sec_context_typ sec =
- print_context false None (read_sec_context sec)
-
-let print_any_name = function
- | Term (ConstRef sp) -> print_constant_with_infos sp
- | Term (IndRef (sp,_)) -> print_inductive sp
- | Term (ConstructRef ((sp,_),_)) -> print_inductive sp
- | Term (VarRef sp) -> print_section_variable sp
- | Syntactic kn -> print_syntactic_def kn
- | Dir (DirModule(dirpath,(mp,_))) -> print_module (printable_body dirpath) mp
+let print_sec_context env sigma sec =
+ print_context env sigma true None (read_sec_context sec)
+
+let print_sec_context_typ env sigma sec =
+ print_context env sigma false None (read_sec_context sec)
+
+let maybe_error_reject_univ_decl na udecl =
+ match na, udecl with
+ | _, None | Term (ConstRef _ | IndRef _ | ConstructRef _), Some _ -> ()
+ | (Term (VarRef _) | Syntactic _ | Dir _ | ModuleType _ | Other _ | Undefined _), Some udecl ->
+ (* TODO Print na somehow *)
+ user_err ~hdr:"reject_univ_decl" (str "This object does not support universe names.")
+
+let print_any_name env sigma na udecl =
+ maybe_error_reject_univ_decl na udecl;
+ match na with
+ | Term (ConstRef sp) -> print_constant_with_infos sp udecl
+ | Term (IndRef (sp,_)) -> print_inductive sp udecl
+ | Term (ConstructRef ((sp,_),_)) -> print_inductive sp udecl
+ | Term (VarRef sp) -> print_section_variable env sigma sp
+ | Syntactic kn -> print_syntactic_def env kn
+ | Dir (DirModule { obj_dir; obj_mp; _ } ) -> print_module (printable_body obj_dir) obj_mp
| Dir _ -> mt ()
| ModuleType mp -> print_modtype mp
| Other (obj, info) -> info.print obj
@@ -807,31 +819,32 @@ let print_any_name = function
try (* Var locale de but, pas var de section... donc pas d'implicits *)
let dir,str = repr_qualid qid in
if not (DirPath.is_empty dir) then raise Not_found;
- str |> Global.lookup_named |> print_named_decl
+ str |> Global.lookup_named |> print_named_decl env sigma
with Not_found ->
user_err
~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.")
-let print_name = function
+let print_name env sigma na udecl =
+ match na with
| ByNotation (loc,(ntn,sc)) ->
- print_any_name
+ print_any_name env sigma
(Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
ntn sc))
+ udecl
| AN ref ->
- print_any_name (locate_any_name ref)
+ print_any_name env sigma (locate_any_name ref) udecl
-let print_opaque_name qid =
- let env = Global.env () in
+let print_opaque_name env sigma qid =
match Nametab.global qid with
| ConstRef cst ->
let cb = Global.lookup_constant cst in
if Declareops.constant_has_body cb then
- print_constant_with_infos cst
+ print_constant_with_infos cst None
else
user_err Pp.(str "Not a defined constant.")
| IndRef (sp,_) ->
- print_inductive sp
+ print_inductive sp None
| ConstructRef cstr as gr ->
let ty, ctx = Global.type_of_global_in_context env gr in
let inst = Univ.AUContext.instance ctx in
@@ -840,15 +853,16 @@ let print_opaque_name qid =
let open EConstr in
print_typed_value (mkConstruct cstr, ty)
| VarRef id ->
- env |> lookup_named id |> print_named_decl
+ env |> lookup_named id |> print_named_decl env sigma
-let print_about_any ?loc k =
+let print_about_any ?loc env sigma k udecl =
+ maybe_error_reject_univ_decl k udecl;
match k with
| Term ref ->
let rb = Reductionops.ReductionBehaviour.print ref in
Dumpglob.add_glob ?loc ref;
pr_infos_list
- (print_ref false ref :: blankline ::
+ (print_ref false ref udecl :: blankline ::
print_name_infos ref @
(if Pp.ismt rb then [] else [rb]) @
print_opacity ref @
@@ -858,23 +872,24 @@ let print_about_any ?loc k =
| [],Notation_term.NRef ref -> Dumpglob.add_glob ?loc ref
| _ -> () in
v 0 (
- print_syntactic_def kn ++ fnl () ++
+ print_syntactic_def env kn ++ fnl () ++
hov 0 (str "Expands to: " ++ pr_located_qualid k))
| Dir _ | ModuleType _ | Undefined _ ->
hov 0 (pr_located_qualid k)
| Other (obj, info) -> hov 0 (info.about obj)
-let print_about = function
+let print_about env sigma na udecl =
+ match na with
| ByNotation (loc,(ntn,sc)) ->
- print_about_any ?loc
+ print_about_any ?loc env sigma
(Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
- ntn sc))
+ ntn sc)) udecl
| AN ref ->
- print_about_any ?loc:(loc_of_reference ref) (locate_any_name ref)
+ print_about_any ?loc:(loc_of_reference ref) env sigma (locate_any_name ref) udecl
(* for debug *)
-let inspect depth =
- print_context false (Some depth) (Lib.contents ())
+let inspect env sigma depth =
+ print_context env sigma false (Some depth) (Lib.contents ())
(*************************************************************************)
@@ -882,18 +897,20 @@ let inspect depth =
open Classops
-let print_coercion_value v = pr_lconstr (get_coercion_value v)
+let print_coercion_value env sigma v = pr_lconstr_env env sigma (get_coercion_value v)
let print_class i =
let cl,_ = class_info_from_index i in
pr_class cl
let print_path ((i,j),p) =
+ let sigma, env = Pfedit.get_current_context () in
hov 2 (
- str"[" ++ hov 0 (prlist_with_sep pr_semicolon print_coercion_value p) ++
+ str"[" ++ hov 0 (prlist_with_sep pr_semicolon (print_coercion_value env sigma) p) ++
str"] : ") ++
print_class i ++ str" >-> " ++ print_class j
+(* XXX: This is suspicious!!! *)
let _ = Classops.install_path_printer print_path
let print_graph () =
@@ -902,8 +919,8 @@ let print_graph () =
let print_classes () =
pr_sequence pr_class (classes())
-let print_coercions () =
- pr_sequence print_coercion_value (coercions())
+let print_coercions env sigma =
+ pr_sequence (print_coercion_value env sigma) (coercions())
let index_of_class cl =
try
@@ -925,11 +942,11 @@ let print_path_between cls clt =
in
print_path ((i,j),p)
-let print_canonical_projections () =
+let print_canonical_projections env sigma =
prlist_with_sep fnl
(fun ((r1,r2),o) -> pr_cs_pattern r2 ++
str " <- " ++
- pr_global r1 ++ str " ( " ++ pr_lconstr o.o_DEF ++ str " )")
+ pr_global r1 ++ str " ( " ++ pr_lconstr_env env sigma o.o_DEF ++ str " )")
(canonical_projections ())
(*************************************************************************)
@@ -940,7 +957,7 @@ let print_canonical_projections () =
open Typeclasses
let pr_typeclass env t =
- print_ref false t.cl_impl
+ print_ref false t.cl_impl None
let print_typeclasses () =
let env = Global.env () in
@@ -949,7 +966,7 @@ let print_typeclasses () =
let pr_instance env i =
(* gallina_print_constant_with_infos i.is_impl *)
(* lighter *)
- print_ref false (instance_impl i) ++
+ print_ref false (instance_impl i) None ++
begin match hint_priority i with
| None -> mt ()
| Some i -> spc () ++ str "|" ++ spc () ++ int i
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 31fd766ea3..8f3a6ddc47 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -18,37 +18,39 @@ open Misctypes
val assumptions_for_print : Name.t list -> Termops.names_context
val print_closed_sections : bool ref
-val print_context : bool -> int option -> Lib.library_segment -> Pp.t
-val print_library_entry : bool -> (object_name * Lib.node) -> Pp.t option
-val print_full_context : unit -> Pp.t
-val print_full_context_typ : unit -> Pp.t
-val print_full_pure_context : unit -> Pp.t
-val print_sec_context : reference -> Pp.t
-val print_sec_context_typ : reference -> Pp.t
+val print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t
+val print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option
+val print_full_context : env -> Evd.evar_map -> Pp.t
+val print_full_context_typ : env -> Evd.evar_map -> Pp.t
+val print_full_pure_context : env -> Evd.evar_map -> Pp.t
+val print_sec_context : env -> Evd.evar_map -> reference -> Pp.t
+val print_sec_context_typ : env -> Evd.evar_map -> reference -> Pp.t
val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> Pp.t
val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> Pp.t
val print_eval :
reduction_function -> env -> Evd.evar_map ->
Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t
-val print_name : reference or_by_notation -> Pp.t
-val print_opaque_name : reference -> Pp.t
-val print_about : reference or_by_notation -> Pp.t
+val print_name : env -> Evd.evar_map -> reference or_by_notation ->
+ Vernacexpr.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 ->
+ Vernacexpr.univ_name_list option -> Pp.t
val print_impargs : reference or_by_notation -> Pp.t
(** Pretty-printing functions for classes and coercions *)
val print_graph : unit -> Pp.t
val print_classes : unit -> Pp.t
-val print_coercions : unit -> Pp.t
+val print_coercions : env -> Evd.evar_map -> Pp.t
val print_path_between : Classops.cl_typ -> Classops.cl_typ -> Pp.t
-val print_canonical_projections : unit -> Pp.t
+val print_canonical_projections : env -> Evd.evar_map -> Pp.t
(** Pretty-printing functions for type classes and instances *)
val print_typeclasses : unit -> Pp.t
val print_instances : global_reference -> Pp.t
val print_all_instances : unit -> Pp.t
-val inspect : int -> Pp.t
+val inspect : env -> Evd.evar_map -> int -> Pp.t
(** {5 Locate} *)
@@ -80,17 +82,17 @@ val print_located_module : reference -> Pp.t
val print_located_other : string -> reference -> Pp.t
type object_pr = {
- print_inductive : MutInd.t -> Pp.t;
- print_constant_with_infos : Constant.t -> Pp.t;
- print_section_variable : variable -> Pp.t;
- print_syntactic_def : KerName.t -> Pp.t;
+ print_inductive : MutInd.t -> Universes.univ_name_list option -> Pp.t;
+ print_constant_with_infos : Constant.t -> Universes.univ_name_list option -> Pp.t;
+ print_section_variable : env -> Evd.evar_map -> variable -> Pp.t;
+ print_syntactic_def : env -> KerName.t -> Pp.t;
print_module : bool -> ModPath.t -> Pp.t;
print_modtype : ModPath.t -> Pp.t;
- print_named_decl : Context.Named.Declaration.t -> Pp.t;
- print_library_entry : bool -> (object_name * Lib.node) -> Pp.t option;
- print_context : bool -> int option -> Lib.library_segment -> Pp.t;
+ print_named_decl : env -> Evd.evar_map -> Context.Named.Declaration.t -> Pp.t;
+ print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option;
+ print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t;
print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t;
- print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t
+ print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t;
}
val set_object_pr : object_pr -> unit
diff --git a/printing/printer.ml b/printing/printer.ml
index 075b03b7d1..6a0597860c 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -10,7 +10,6 @@ open Pp
open CErrors
open Util
open Names
-open Term
open Constr
open Environ
open Globnames
@@ -26,9 +25,6 @@ module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
module CompactedDecl = Context.Compacted.Declaration
-let get_current_context () =
- Pfedit.get_current_context ()
-
let enable_unfocused_goal_printing = ref false
let enable_goal_tags_printing = ref false
let enable_goal_names_printing = ref false
@@ -104,10 +100,10 @@ let pr_econstr_env env sigma c = pr_econstr_core false env sigma c
(* NB do not remove the eta-redexes! Global.env() has side-effects... *)
let pr_lconstr t =
- let (sigma, env) = get_current_context () in
+ let (sigma, env) = Pfedit.get_current_context () in
pr_lconstr_env env sigma t
let pr_constr t =
- let (sigma, env) = get_current_context () in
+ let (sigma, env) = Pfedit.get_current_context () in
pr_constr_env env sigma t
let pr_open_lconstr (_,c) = pr_lconstr c
@@ -127,10 +123,10 @@ let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_econstr_env
let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_leconstr_env
let pr_constr_under_binders c =
- let (sigma, env) = get_current_context () in
+ let (sigma, env) = Pfedit.get_current_context () in
pr_constr_under_binders_env env sigma c
let pr_lconstr_under_binders c =
- let (sigma, env) = get_current_context () in
+ let (sigma, env) = Pfedit.get_current_context () in
pr_lconstr_under_binders_env env sigma c
let pr_etype_core goal_concl_style env sigma t =
@@ -142,10 +138,10 @@ let pr_ltype_env env sigma c = pr_letype_core false env sigma (EConstr.of_constr
let pr_type_env env sigma c = pr_etype_core false env sigma (EConstr.of_constr c)
let pr_ltype t =
- let (sigma, env) = get_current_context () in
+ let (sigma, env) = Pfedit.get_current_context () in
pr_ltype_env env sigma t
let pr_type t =
- let (sigma, env) = get_current_context () in
+ let (sigma, env) = Pfedit.get_current_context () in
pr_type_env env sigma t
let pr_etype_env env sigma c = pr_etype_core false env sigma c
@@ -156,7 +152,7 @@ let pr_ljudge_env env sigma j =
(pr_leconstr_env env sigma j.uj_val, pr_leconstr_env env sigma j.uj_type)
let pr_ljudge j =
- let (sigma, env) = get_current_context () in
+ let (sigma, env) = Pfedit.get_current_context () in
pr_ljudge_env env sigma j
let pr_lglob_constr_env env c =
@@ -165,10 +161,10 @@ let pr_glob_constr_env env c =
pr_constr_expr (extern_glob_constr (Termops.vars_of_env env) c)
let pr_lglob_constr c =
- let (sigma, env) = get_current_context () in
+ let (sigma, env) = Pfedit.get_current_context () in
pr_lglob_constr_env env c
let pr_glob_constr c =
- let (sigma, env) = get_current_context () in
+ let (sigma, env) = Pfedit.get_current_context () in
pr_glob_constr_env env c
let pr_closed_glob_n_env env sigma n c =
@@ -176,7 +172,7 @@ let pr_closed_glob_n_env env sigma n c =
let pr_closed_glob_env env sigma c =
pr_constr_expr (extern_closed_glob false env sigma c)
let pr_closed_glob c =
- let (sigma, env) = get_current_context () in
+ let (sigma, env) = Pfedit.get_current_context () in
pr_closed_glob_env env sigma c
let pr_lconstr_pattern_env env sigma c =
@@ -188,10 +184,10 @@ let pr_cases_pattern t =
pr_cases_pattern_expr (extern_cases_pattern Names.Id.Set.empty t)
let pr_lconstr_pattern t =
- let (sigma, env) = get_current_context () in
+ let (sigma, env) = Pfedit.get_current_context () in
pr_lconstr_pattern_env env sigma t
let pr_constr_pattern t =
- let (sigma, env) = get_current_context () in
+ let (sigma, env) = Pfedit.get_current_context () in
pr_constr_pattern_env env sigma t
let pr_sort sigma s = pr_glob_sort (extern_sort sigma s)
@@ -253,13 +249,20 @@ let safe_gen f env sigma c =
let safe_pr_lconstr_env = safe_gen pr_lconstr_env
let safe_pr_constr_env = safe_gen pr_constr_env
let safe_pr_lconstr t =
- let (sigma, env) = get_current_context () in
+ let (sigma, env) = Pfedit.get_current_context () in
safe_pr_lconstr_env env sigma t
let safe_pr_constr t =
- let (sigma, env) = get_current_context () in
+ let (sigma, env) = Pfedit.get_current_context () in
safe_pr_constr_env env sigma t
+let pr_universe_ctx_set sigma c =
+ if !Detyping.print_universes && not (Univ.ContextSet.is_empty c) then
+ fnl()++pr_in_comment (fun c -> v 0
+ (Univ.pr_universe_context_set (Termops.pr_evd_level sigma) c)) c
+ else
+ mt()
+
let pr_universe_ctx sigma c =
if !Detyping.print_universes && not (Univ.UContext.is_empty c) then
fnl()++pr_in_comment (fun c -> v 0
@@ -267,6 +270,10 @@ let pr_universe_ctx sigma c =
else
mt()
+let pr_constant_universes sigma = function
+ | Entries.Monomorphic_const_entry ctx -> pr_universe_ctx_set sigma ctx
+ | Entries.Polymorphic_const_entry ctx -> pr_universe_ctx sigma ctx
+
let pr_cumulativity_info sigma cumi =
if !Detyping.print_universes
&& not (Univ.UContext.is_empty (Univ.CumulativityInfo.univ_context cumi)) then
@@ -587,7 +594,7 @@ let default_pr_subgoal n sigma =
in
prrec n
-let pr_internal_existential_key ev = str (string_of_existential ev)
+let pr_internal_existential_key ev = Evar.print ev
let print_evar_constraints gl sigma =
let pr_env =
@@ -766,7 +773,7 @@ let default_pr_subgoals ?(pr_first=true)
type printer_pr = {
- pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t;
+ pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> Evar.t list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t;
pr_subgoal : int -> evar_map -> goal list -> Pp.t;
pr_goal : goal sigma -> Pp.t;
}
@@ -788,7 +795,7 @@ let pr_goal x = !printer_pr.pr_goal x
(* End abstraction layer *)
(**********************************************************************)
-let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
+let pr_open_subgoals ~proof =
(* spiwack: it shouldn't be the job of the printer to look up stuff
in the [evar_map], I did stuff that way because it was more
straightforward, but seriously, [Proof.proof] should return
@@ -826,15 +833,13 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
pr_subgoals ~pr_first:true None bsigma seeds shelf [] unfocused_if_needed bgoals_focused
end
-let pr_nth_open_subgoal n =
- let pf = Proof_global.give_me_the_proof () in
- let { it=gls ; sigma=sigma } = Proof.V82.subgoals pf in
+let pr_nth_open_subgoal ~proof n =
+ let gls,_,_,_,sigma = Proof.proof proof in
pr_subgoal n sigma gls
-let pr_goal_by_id id =
- let p = Proof_global.give_me_the_proof () in
+let pr_goal_by_id ~proof id =
try
- Proof.in_proof p (fun sigma ->
+ Proof.in_proof proof (fun sigma ->
let g = Evd.evar_key id sigma in
pr_selected_subgoal (pr_id id) sigma g)
with Not_found -> user_err Pp.(str "No such goal.")
@@ -916,7 +921,7 @@ let pr_assumptionset env s =
with e when CErrors.noncritical e -> mt ()
in
let safe_pr_ltype_relctx (rctx, typ) =
- let sigma, env = get_current_context () in
+ let sigma, env = Pfedit.get_current_context () in
let env = Environ.push_rel_context rctx env in
try str " " ++ pr_ltype_env env sigma typ
with e when CErrors.noncritical e -> mt ()
diff --git a/printing/printer.mli b/printing/printer.mli
index fbba14edea..36ca1bdcca 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -27,10 +27,12 @@ val enable_goal_names_printing : bool ref
val pr_lconstr_env : env -> evar_map -> constr -> Pp.t
val pr_lconstr : constr -> Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
val pr_lconstr_goal_style_env : env -> evar_map -> constr -> Pp.t
val pr_constr_env : env -> evar_map -> constr -> Pp.t
val pr_constr : constr -> Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
val pr_constr_goal_style_env : env -> evar_map -> constr -> Pp.t
val pr_constr_n_env : env -> evar_map -> Notation_term.tolerability -> constr -> Pp.t
@@ -41,14 +43,18 @@ val pr_constr_n_env : env -> evar_map -> Notation_term.tolerability -> co
val safe_pr_lconstr_env : env -> evar_map -> constr -> Pp.t
val safe_pr_lconstr : constr -> Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
val safe_pr_constr_env : env -> evar_map -> constr -> Pp.t
val safe_pr_constr : constr -> Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
val pr_econstr_env : env -> evar_map -> EConstr.t -> Pp.t
val pr_econstr : EConstr.t -> Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
val pr_leconstr_env : env -> evar_map -> EConstr.t -> Pp.t
val pr_leconstr : EConstr.t -> Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
val pr_econstr_n_env : env -> evar_map -> Notation_term.tolerability -> EConstr.t -> Pp.t
@@ -57,41 +63,53 @@ val pr_letype_env : env -> evar_map -> EConstr.types -> Pp.t
val pr_open_constr_env : env -> evar_map -> open_constr -> Pp.t
val pr_open_constr : open_constr -> Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
val pr_open_lconstr_env : env -> evar_map -> open_constr -> Pp.t
val pr_open_lconstr : open_constr -> Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
val pr_constr_under_binders_env : env -> evar_map -> constr_under_binders -> Pp.t
val pr_constr_under_binders : constr_under_binders -> Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> Pp.t
val pr_lconstr_under_binders : constr_under_binders -> Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
val pr_goal_concl_style_env : env -> evar_map -> EConstr.types -> Pp.t
val pr_ltype_env : env -> evar_map -> types -> Pp.t
val pr_ltype : types -> Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
val pr_type_env : env -> evar_map -> types -> Pp.t
val pr_type : types -> Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
val pr_closed_glob_n_env : env -> evar_map -> Notation_term.tolerability -> closed_glob_constr -> Pp.t
val pr_closed_glob_env : env -> evar_map -> closed_glob_constr -> Pp.t
val pr_closed_glob : closed_glob_constr -> Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
val pr_ljudge_env : env -> evar_map -> EConstr.unsafe_judgment -> Pp.t * Pp.t
val pr_ljudge : EConstr.unsafe_judgment -> Pp.t * Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
val pr_lglob_constr_env : env -> 'a glob_constr_g -> Pp.t
val pr_lglob_constr : 'a glob_constr_g -> Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
val pr_glob_constr_env : env -> 'a glob_constr_g -> Pp.t
val pr_glob_constr : 'a glob_constr_g -> Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
val pr_lconstr_pattern_env : env -> evar_map -> constr_pattern -> Pp.t
val pr_lconstr_pattern : constr_pattern -> Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
val pr_constr_pattern_env : env -> evar_map -> constr_pattern -> Pp.t
val pr_constr_pattern : constr_pattern -> Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
val pr_cases_pattern : cases_pattern -> Pp.t
@@ -103,6 +121,8 @@ val pr_polymorphic : bool -> Pp.t
val pr_cumulative : bool -> bool -> Pp.t
val pr_universe_instance : evar_map -> Univ.UContext.t -> Pp.t
val pr_universe_ctx : evar_map -> Univ.UContext.t -> Pp.t
+val pr_universe_ctx_set : evar_map -> Univ.ContextSet.t -> Pp.t
+val pr_constant_universes : evar_map -> Entries.constant_universes_entry -> Pp.t
val pr_cumulativity_info : evar_map -> Univ.CumulativityInfo.t -> Pp.t
(** Printing global references using names as short as possible *)
@@ -111,7 +131,7 @@ val pr_global_env : Id.Set.t -> global_reference -> Pp.t
val pr_global : global_reference -> Pp.t
val pr_constant : env -> Constant.t -> Pp.t
-val pr_existential_key : evar_map -> existential_key -> Pp.t
+val pr_existential_key : evar_map -> Evar.t -> Pp.t
val pr_existential : env -> evar_map -> existential -> Pp.t
val pr_constructor : env -> constructor -> Pp.t
val pr_inductive : env -> inductive -> Pp.t
@@ -160,15 +180,15 @@ val pr_goal : goal sigma -> Pp.t
focused goals unless the conrresponding option
[enable_unfocused_goal_printing] is set. [seeds] is for printing
dependent evars (mainly for emacs proof tree mode). *)
-val pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> evar list -> Goal.goal list -> int list
+val pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> Evar.t list -> Goal.goal list -> int list
-> goal list -> goal list -> Pp.t
val pr_subgoal : int -> evar_map -> goal list -> Pp.t
val pr_concl : int -> evar_map -> goal -> Pp.t
-val pr_open_subgoals : ?proof:Proof.proof -> unit -> Pp.t
-val pr_nth_open_subgoal : int -> Pp.t
-val pr_evar : evar_map -> (evar * evar_info) -> Pp.t
+val pr_open_subgoals : proof:Proof.t -> Pp.t
+val pr_nth_open_subgoal : proof:Proof.t -> int -> Pp.t
+val pr_evar : evar_map -> (Evar.t * evar_info) -> Pp.t
val pr_evars_int : evar_map -> int -> evar_info Evar.Map.t -> Pp.t
val pr_evars : evar_map -> evar_info Evar.Map.t -> Pp.t
val pr_ne_evar_set : Pp.t -> Pp.t -> evar_map ->
@@ -200,13 +220,13 @@ module ContextObjectMap : CMap.ExtS
val pr_assumptionset :
env -> types ContextObjectMap.t -> Pp.t
-val pr_goal_by_id : Id.t -> Pp.t
+val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t
type printer_pr = {
- pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t;
+ pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> Evar.t list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t;
pr_subgoal : int -> evar_map -> goal list -> Pp.t;
pr_goal : goal sigma -> Pp.t;
-};;
+}
val set_printer_pr : printer_pr -> unit
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 0abca01602..05292b06ba 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -121,7 +121,7 @@ let instantiate_cumulativity_info cumi =
in
CumulativityInfo.make (expose univs, expose subtyp)
-let print_mutual_inductive env mind mib =
+let print_mutual_inductive env mind mib udecl =
let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x))
in
let keyword =
@@ -131,7 +131,14 @@ let print_mutual_inductive env mind mib =
| BiFinite -> "Variant"
| CoFinite -> "CoInductive"
in
- let bl = Universes.universe_binders_of_global (IndRef (mind, 0)) in
+ let univs =
+ let open Univ in
+ if Declareops.inductive_is_polymorphic mib then
+ Array.to_list (Instance.to_array
+ (AUContext.instance (Declareops.inductive_polymorphic_context mib)))
+ else []
+ in
+ let bl = Universes.universe_binders_with_opt_names (IndRef (mind, 0)) univs udecl in
let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in
hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++
Printer.pr_cumulative
@@ -159,7 +166,7 @@ let get_fields =
in
prodec_rec [] []
-let print_record env mind mib =
+let print_record env mind mib udecl =
let u =
if Declareops.inductive_is_polymorphic mib then
Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib)
@@ -173,7 +180,8 @@ let print_record env mind mib =
let cstrtype = hnf_prod_applist env cstrtypes.(0) args in
let fields = get_fields cstrtype in
let envpar = push_rel_context params env in
- let bl = Universes.universe_binders_of_global (IndRef (mind,0)) in
+ let bl = Universes.universe_binders_with_opt_names (IndRef (mind,0))
+ (Array.to_list (Univ.Instance.to_array u)) udecl in
let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in
let keyword =
let open Decl_kinds in
@@ -205,11 +213,11 @@ let print_record env mind mib =
sigma (instantiate_cumulativity_info cumi)
)
-let pr_mutual_inductive_body env mind mib =
+let pr_mutual_inductive_body env mind mib udecl =
if mib.mind_record <> None && not !Flags.raw_print then
- print_record env mind mib
+ print_record env mind mib udecl
else
- print_mutual_inductive env mind mib
+ print_mutual_inductive env mind mib udecl
(** Modpaths *)
@@ -237,10 +245,10 @@ let print_kn locals kn =
with
Not_found -> print_modpath locals kn
-let nametab_register_dir mp =
+let nametab_register_dir obj_mp =
let id = mk_fake_top () in
- let dir = DirPath.make [id] in
- Nametab.push_dir (Nametab.Until 1) dir (DirModule (dir,(mp,DirPath.empty)))
+ let obj_dir = DirPath.make [id] in
+ Nametab.push_dir (Nametab.Until 1) obj_dir (DirModule { obj_dir; obj_mp; obj_sec = DirPath.empty })
(** Nota: the [global_reference] we register in the nametab below
might differ from internal ones, since we cannot recreate here
@@ -335,7 +343,7 @@ let print_body is_impl env mp (l,body) =
| SFBmind mib ->
try
let env = Option.get env in
- pr_mutual_inductive_body env (MutInd.make2 mp l) mib
+ pr_mutual_inductive_body env (MutInd.make2 mp l) mib None
with e when CErrors.noncritical e ->
let keyword =
let open Decl_kinds in
@@ -374,9 +382,12 @@ let rec print_typ_expr env mp locals mty =
| MEwith(me,WithDef(idl,(c, _)))->
let env' = None in (* TODO: build a proper environment if env <> None *)
let s = String.concat "." (List.map Id.to_string idl) in
+ (* XXX: What should env and sigma be here? *)
+ let env = Global.env () in
+ let sigma = Evd.empty in
hov 2 (print_typ_expr env' mp locals me ++ spc() ++ str "with" ++ spc()
++ def "Definition"++ spc() ++ str s ++ spc() ++ str ":="++ spc()
- ++ Printer.pr_lconstr c)
+ ++ Printer.pr_lconstr_env env sigma c)
| MEwith(me,WithMod(idl,mp'))->
let s = String.concat "." (List.map Id.to_string idl) in
hov 2 (print_typ_expr env mp locals me ++ spc() ++ str "with" ++ spc() ++
diff --git a/printing/printmod.mli b/printing/printmod.mli
index b0bbb21e05..97ed063fe3 100644
--- a/printing/printmod.mli
+++ b/printing/printmod.mli
@@ -11,6 +11,8 @@ open Names
(** false iff the module is an element of an open module type *)
val printable_body : DirPath.t -> bool
-val pr_mutual_inductive_body : Environ.env -> MutInd.t -> Declarations.mutual_inductive_body -> Pp.t
+val pr_mutual_inductive_body : Environ.env ->
+ MutInd.t -> Declarations.mutual_inductive_body ->
+ Vernacexpr.univ_name_list option -> Pp.t
val print_module : bool -> ModPath.t -> Pp.t
val print_modtype : ModPath.t -> Pp.t
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 23:49:36 +0000