aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/ppconstr.ml3
-rw-r--r--printing/ppvernac.ml25
-rw-r--r--printing/prettyp.ml11
-rw-r--r--printing/printer.ml4
-rw-r--r--printing/printer.mli3
-rw-r--r--printing/printmod.ml3
6 files changed, 27 insertions, 22 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 51735bc9e1..1146b42a01 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -732,6 +732,9 @@ let tag_var = tag Tag.variable
return (pr_prim_token p, prec_of_prim_token p)
| CDelimiters (sc,a) ->
return (pr_delimiters sc (pr mt (ldelim,E) a), ldelim)
+ | CProj (p,c) ->
+ let p = pr_proj (pr mt) pr_app c (CAst.make (CRef (p,None))) [] in
+ return (p, lproj)
in
let loc = constr_loc a in
pr_with_comments ?loc
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 96e39e89a6..950246c531 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -31,12 +31,6 @@ open Decl_kinds
let pr_lconstr = pr_lconstr_expr
let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr
- let pr_lident (loc,id) =
- match loc with
- | None -> pr_id id
- | Some loc -> let (b,_) = Loc.unloc loc in
- pr_located pr_id @@ Loc.tag ~loc:(Loc.make_loc (b,b + String.length (Id.to_string id))) id
-
let pr_uconstraint (l, d, r) =
pr_glob_level l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++
pr_glob_level r
@@ -77,9 +71,8 @@ open Decl_kinds
| Some loc -> let (b,_) = Loc.unloc loc in
pr_located pr_fqid @@ Loc.tag ~loc:(Loc.make_loc (b,b + String.length (string_of_fqid fqid))) fqid
- let pr_lname = function
- | (loc,Name id) -> pr_lident (loc,id)
- | lna -> pr_located Name.print lna
+ let pr_lname_decl (n, u) =
+ pr_lname n ++ pr_universe_decl u
let pr_smart_global = Pputils.pr_or_by_notation pr_reference
@@ -398,8 +391,6 @@ open Decl_kinds
++ prlist (pr_decl_notation pr_constr) ntn
let pr_statement head (idpl,(bl,c)) =
- assert (not (Option.is_empty idpl));
- let idpl = Option.get idpl in
hov 2
(head ++ spc() ++ pr_ident_decl idpl ++ spc() ++
(match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
@@ -572,8 +563,6 @@ open Decl_kinds
return (keyword "Unfocus")
| VernacUnfocused ->
return (keyword "Unfocused")
- | VernacGoal c ->
- return (keyword "Goal" ++ pr_lconstrarg c)
| VernacAbort id ->
return (keyword "Abort" ++ pr_opt pr_lident id)
| VernacUndo i ->
@@ -684,7 +673,10 @@ open Decl_kinds
(* Gallina *)
| VernacDefinition ((discharge,kind),id,b) -> (* A verifier... *)
let pr_def_token dk =
- keyword (Kindops.string_of_definition_object_kind dk)
+ keyword (
+ if Name.is_anonymous (snd (fst id))
+ then "Goal"
+ else Kindops.string_of_definition_object_kind dk)
in
let pr_reduce = function
| None -> mt()
@@ -701,12 +693,13 @@ open Decl_kinds
in
(pr_binders_arg bl,ty,Some (pr_reduce red ++ pr_lconstr body))
| ProveBody (bl,t) ->
- (pr_binders_arg bl, str" :" ++ pr_spc_lconstr t, None) in
+ let typ u = if snd (fst id) = Anonymous then (assert (bl = []); u) else (str" :" ++ u) in
+ (pr_binders_arg bl, typ (pr_spc_lconstr t), None) in
let (binds,typ,c) = pr_def_body b in
return (
hov 2 (
pr_def_token kind ++ spc()
- ++ pr_ident_decl id ++ binds ++ typ
+ ++ pr_lname_decl id ++ binds ++ typ
++ (match c with
| None -> mt()
| Some cc -> str" :=" ++ spc() ++ cc))
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 2b7886d115..114a071eee 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -78,6 +78,15 @@ let print_ref reduce ref udecl =
in EConstr.it_mkProd_or_LetIn ccl ctx
else typ in
let univs = Global.universes_of_global ref in
+ let variance = match ref with
+ | VarRef _ | ConstRef _ -> None
+ | IndRef (ind,_) | ConstructRef ((ind,_),_) ->
+ let mind = Environ.lookup_mind ind (Global.env ()) in
+ begin match mind.Declarations.mind_universes with
+ | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> None
+ | Declarations.Cumulative_ind cumi -> Some (Univ.ACumulativityInfo.variance cumi)
+ end
+ in
let inst = Univ.AUContext.instance univs in
let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in
let env = Global.env () in
@@ -89,7 +98,7 @@ let print_ref reduce ref udecl =
else mt ()
in
hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++
- Printer.pr_universe_ctx sigma univs)
+ Printer.pr_universe_ctx sigma ?variance univs)
(********************************)
(** Printing implicit arguments *)
diff --git a/printing/printer.ml b/printing/printer.ml
index a63004cebe..d720bc2f8c 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -263,10 +263,10 @@ let pr_universe_ctx_set sigma c =
else
mt()
-let pr_universe_ctx sigma c =
+let pr_universe_ctx sigma ?variance c =
if !Detyping.print_universes && not (Univ.UContext.is_empty c) then
fnl()++pr_in_comment (fun c -> v 0
- (Univ.pr_universe_context (Termops.pr_evd_level sigma) c)) c
+ (Univ.pr_universe_context (Termops.pr_evd_level sigma) ?variance c)) c
else
mt()
diff --git a/printing/printer.mli b/printing/printer.mli
index 804014745c..a3427920af 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -120,7 +120,8 @@ val pr_sort : evar_map -> Sorts.t -> Pp.t
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 : evar_map -> ?variance:Univ.Variance.t array ->
+ 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
diff --git a/printing/printmod.ml b/printing/printmod.ml
index fb9d45a793..35487e09c1 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -113,13 +113,12 @@ let print_one_inductive env sigma mib ((_,i) as ind) =
let instantiate_cumulativity_info cumi =
let open Univ in
let univs = ACumulativityInfo.univ_context cumi in
- let subtyp = ACumulativityInfo.subtyp_context cumi in
let expose ctx =
let inst = AUContext.instance ctx in
let cst = AUContext.instantiate inst ctx in
UContext.make (inst, cst)
in
- CumulativityInfo.make (expose univs, expose subtyp)
+ CumulativityInfo.make (expose univs, ACumulativityInfo.variance cumi)
let print_mutual_inductive env mind mib udecl =
let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x))
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-07 03:18:06 +0000