aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/genprint.ml2
-rw-r--r--printing/genprint.mli2
-rw-r--r--printing/miscprint.ml74
-rw-r--r--printing/miscprint.mli37
-rw-r--r--printing/ppconstr.ml2
-rw-r--r--printing/ppconstr.mli2
-rw-r--r--printing/pputils.ml2
-rw-r--r--printing/pputils.mli2
-rw-r--r--printing/ppvernac.ml8
-rw-r--r--printing/ppvernac.mli2
-rw-r--r--printing/prettyp.ml59
-rw-r--r--printing/prettyp.mli2
-rw-r--r--printing/printer.ml4
-rw-r--r--printing/printer.mli2
-rw-r--r--printing/printmod.ml32
-rw-r--r--printing/printmod.mli2
16 files changed, 88 insertions, 146 deletions
diff --git a/printing/genprint.ml b/printing/genprint.ml
index 6505a8f826..bb9736d731 100644
--- a/printing/genprint.ml
+++ b/printing/genprint.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/genprint.mli b/printing/genprint.mli
index 5381fc5bdb..24779a359d 100644
--- a/printing/genprint.mli
+++ b/printing/genprint.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/miscprint.ml b/printing/miscprint.ml
deleted file mode 100644
index a4ecbdf5e5..0000000000
--- a/printing/miscprint.ml
+++ /dev/null
@@ -1,74 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Misctypes
-open Pp
-
-(** Printing of [intro_pattern] *)
-
-let rec pr_intro_pattern prc (_,pat) = match pat with
- | IntroForthcoming true -> str "*"
- | IntroForthcoming false -> str "**"
- | IntroNaming p -> pr_intro_pattern_naming p
- | IntroAction p -> pr_intro_pattern_action prc p
-
-and pr_intro_pattern_naming = function
- | IntroIdentifier id -> Nameops.pr_id id
- | IntroFresh id -> str "?" ++ Nameops.pr_id id
- | IntroAnonymous -> str "?"
-
-and pr_intro_pattern_action prc = function
- | IntroWildcard -> str "_"
- | IntroOrAndPattern pll -> pr_or_and_intro_pattern prc pll
- | IntroInjection pl ->
- str "[=" ++ hv 0 (prlist_with_sep spc (pr_intro_pattern prc) pl) ++
- str "]"
- | IntroApplyOn ((_,c),pat) -> pr_intro_pattern prc pat ++ str "%" ++ prc c
- | IntroRewrite true -> str "->"
- | IntroRewrite false -> str "<-"
-
-and pr_or_and_intro_pattern prc = function
- | IntroAndPattern pl ->
- str "(" ++ hv 0 (prlist_with_sep pr_comma (pr_intro_pattern prc) pl) ++ str ")"
- | IntroOrPattern pll ->
- str "[" ++
- hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc (pr_intro_pattern prc)) pll)
- ++ str "]"
-
-(** Printing of [move_location] *)
-
-let pr_move_location pr_id = function
- | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id
- | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id
- | MoveFirst -> str " at top"
- | MoveLast -> str " at bottom"
-
-(** Printing of bindings *)
-let pr_binding prc = function
- | loc, (NamedHyp id, c) -> hov 1 (Names.Id.print id ++ str " := " ++ cut () ++ prc c)
- | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
-
-let pr_bindings prc prlc = function
- | ImplicitBindings l ->
- brk (1,1) ++ str "with" ++ brk (1,1) ++
- pr_sequence prc l
- | ExplicitBindings l ->
- brk (1,1) ++ str "with" ++ brk (1,1) ++
- pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
- | NoBindings -> mt ()
-
-let pr_bindings_no_with prc prlc = function
- | ImplicitBindings l ->
- brk (0,1) ++ prlist_with_sep spc prc l
- | ExplicitBindings l ->
- brk (0,1) ++ prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
- | NoBindings -> mt ()
-
-let pr_with_bindings prc prlc (c,bl) =
- hov 1 (prc c ++ pr_bindings prc prlc bl)
-
diff --git a/printing/miscprint.mli b/printing/miscprint.mli
deleted file mode 100644
index dbbe3dcfd8..0000000000
--- a/printing/miscprint.mli
+++ /dev/null
@@ -1,37 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Misctypes
-
-(** Printing of [intro_pattern] *)
-
-val pr_intro_pattern :
- ('a -> Pp.std_ppcmds) -> 'a intro_pattern_expr Loc.located -> Pp.std_ppcmds
-
-val pr_or_and_intro_pattern :
- ('a -> Pp.std_ppcmds) -> 'a or_and_intro_pattern_expr -> Pp.std_ppcmds
-
-val pr_intro_pattern_naming : intro_pattern_naming_expr -> Pp.std_ppcmds
-
-(** Printing of [move_location] *)
-
-val pr_move_location :
- ('a -> Pp.std_ppcmds) -> 'a move_location -> Pp.std_ppcmds
-
-val pr_bindings :
- ('a -> Pp.std_ppcmds) ->
- ('a -> Pp.std_ppcmds) -> 'a bindings -> Pp.std_ppcmds
-
-val pr_bindings_no_with :
- ('a -> Pp.std_ppcmds) ->
- ('a -> Pp.std_ppcmds) -> 'a bindings -> Pp.std_ppcmds
-
-val pr_with_bindings :
- ('a -> Pp.std_ppcmds) ->
- ('a -> Pp.std_ppcmds) -> 'a * 'a bindings -> Pp.std_ppcmds
-
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 49eedb767b..cf513321fb 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 482c994c25..fd232759ef 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/pputils.ml b/printing/pputils.ml
index 99d07601c4..9ef9162aee 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/pputils.mli b/printing/pputils.mli
index b236fed702..0dee11e0bc 100644
--- a/printing/pputils.mli
+++ b/printing/pputils.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index d0536a1744..a68b569cbe 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -105,7 +105,7 @@ open Decl_kinds
| SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
let pr_search a gopt b pr_p =
- pr_opt (fun g -> Proof_global.pr_goal_selector g ++ str ":"++ spc()) gopt
+ pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt
++
match a with
| SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b
@@ -490,7 +490,7 @@ open Decl_kinds
| PrintVisibility s ->
keyword "Print Visibility" ++ pr_opt str s
| PrintAbout (qid,gopt) ->
- pr_opt (fun g -> Proof_global.pr_goal_selector g ++ str ":"++ spc()) gopt
+ pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt
++ keyword "About" ++ spc() ++ pr_smart_global qid
| PrintImplicit qid ->
keyword "Print Implicit" ++ spc() ++ pr_smart_global qid
@@ -1132,7 +1132,7 @@ open Decl_kinds
| None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c)
in
let pr_i = match io with None -> mt ()
- | Some i -> Proof_global.pr_goal_selector i ++ str ": " in
+ | Some i -> Proof_bullet.pr_goal_selector i ++ str ": " in
return (pr_i ++ pr_mayeval r c)
| VernacGlobalCheck c ->
return (hov 2 (keyword "Type" ++ pr_constrarg c))
diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli
index 836b05e0e4..ed5585b309 100644
--- a/printing/ppvernac.mli
+++ b/printing/ppvernac.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 6d2bf6b73a..827c0e4583 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -70,7 +70,8 @@ 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 typ = Global.type_of_global_unsafe ref in
+ 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
let typ =
if reduce then
@@ -78,6 +79,8 @@ let print_ref reduce ref =
in EConstr.it_mkProd_or_LetIn ccl ctx
else typ in
let univs = Global.universes_of_global ref 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
let bl = Universes.universe_binders_of_global ref in
let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in
@@ -135,7 +138,7 @@ let print_renames_list prefix l =
hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map Name.print l))]
let need_expansion impl ref =
- let typ = Global.type_of_global_unsafe ref in
+ let typ, _ = Global.type_of_global_in_context (Global.env ()) ref in
let ctx = prod_assum typ in
let nprods = List.count is_local_assum ctx in
not (List.is_empty impl) && List.length impl >= nprods &&
@@ -503,15 +506,48 @@ let ungeneralized_type_of_constant_type t =
let print_instance sigma cb =
if Declareops.constant_is_polymorphic cb then
- pr_universe_instance sigma (Declareops.constant_polymorphic_context cb)
+ let univs = Declareops.constant_polymorphic_context cb in
+ let inst = Univ.AUContext.instance univs in
+ let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in
+ pr_universe_instance sigma univs
else mt()
let print_constant with_values sep sp =
let cb = Global.lookup_constant sp in
let val_0 = Global.body_of_constant_body cb in
- let typ = Declareops.type_of_constant cb in
+ let typ = match cb.const_type with
+ | RegularArity t as x ->
+ begin match cb.const_universes with
+ | Monomorphic_const _ -> x
+ | Polymorphic_const univs ->
+ let inst = Univ.AUContext.instance univs in
+ RegularArity (Vars.subst_instance_constr inst t)
+ end
+ | TemplateArity _ as x -> x
+ in
let typ = ungeneralized_type_of_constant_type typ in
- let univs = Global.universes_of_constant_body cb in
+ let univs =
+ let otab = Global.opaque_tables () in
+ match cb.const_body with
+ | Undef _ | Def _ ->
+ begin
+ match cb.const_universes with
+ | Monomorphic_const ctx -> ctx
+ | Polymorphic_const ctx ->
+ let inst = Univ.AUContext.instance ctx in
+ Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx)
+ 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)
+ | 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)
+ in
let ctx =
Evd.evar_universe_context_of_binders
(Universes.universe_binders_of_global (ConstRef sp))
@@ -525,9 +561,10 @@ let print_constant with_values sep sp =
print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++
str" ]" ++
Printer.pr_universe_ctx 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 (val_0,typ) else pr_ltype typ)++
+ (if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++
Printer.pr_universe_ctx sigma univs)
let gallina_print_constant_with_infos sp =
@@ -765,9 +802,11 @@ let print_opaque_name qid =
| IndRef (sp,_) ->
print_inductive sp
| ConstructRef cstr as gr ->
- let open EConstr in
- let ty = Universes.unsafe_type_of_global gr in
+ let ty, ctx = Global.type_of_global_in_context env gr in
+ let inst = Univ.AUContext.instance ctx in
+ let ty = Vars.subst_instance_constr inst ty in
let ty = EConstr.of_constr ty in
+ let open EConstr in
print_typed_value (mkConstruct cstr, ty)
| VarRef id ->
env |> lookup_named id |> NamedDecl.set_id id |> print_named_decl
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 6841781ccd..4add21fa7b 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/printer.ml b/printing/printer.ml
index 3b0b6d5d23..3516788022 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -805,7 +805,7 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
| _ , _, _ ->
let end_cmd =
str "This subproof is complete, but there are some unfocused goals." ++
- (let s = Proof_global.Bullet.suggest p in
+ (let s = Proof_bullet.suggest p in
if Pp.ismt s then s else fnl () ++ s) ++
fnl ()
in
diff --git a/printing/printer.mli b/printing/printer.mli
index f0a32bbbdf..f8685b0895 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 08d177f53e..5c7dcdc10f 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -89,7 +89,7 @@ let build_ind_type env mip =
let print_one_inductive env sigma mib ((_,i) as ind) =
let u = if Declareops.inductive_is_polymorphic mib then
- Declareops.inductive_polymorphic_instance mib
+ Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib)
else Univ.Instance.empty in
let mip = mib.mind_packets.(i) in
let params = Inductive.inductive_paramdecls (mib,u) in
@@ -100,7 +100,9 @@ let print_one_inductive env sigma mib ((_,i) as ind) =
let envpar = push_rel_context params env in
let inst =
if Declareops.inductive_is_polymorphic mib then
- Printer.pr_universe_instance sigma (Declareops.inductive_polymorphic_context mib)
+ let ctx = Declareops.inductive_polymorphic_context mib in
+ let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in
+ Printer.pr_universe_instance sigma ctx
else mt ()
in
hov 0 (
@@ -108,6 +110,17 @@ let print_one_inductive env sigma mib ((_,i) as ind) =
str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ str " :=") ++
brk(0,2) ++ print_constructors envpar sigma mip.mind_consnames cstrtypes
+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)
+
let print_mutual_inductive env mind mib =
let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x))
in
@@ -131,7 +144,7 @@ let print_mutual_inductive env mind mib =
| Monomorphic_ind _ | Polymorphic_ind _ -> str ""
| Cumulative_ind cumi ->
Printer.pr_cumulativity_info
- sigma (Univ.instantiate_cumulativity_info cumi))
+ sigma (instantiate_cumulativity_info cumi))
let get_fields =
let rec prodec_rec l subst c =
@@ -149,7 +162,7 @@ let get_fields =
let print_record env mind mib =
let u =
if Declareops.inductive_is_polymorphic mib then
- Declareops.inductive_polymorphic_instance mib
+ Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib)
else Univ.Instance.empty
in
let mip = mib.mind_packets.(0) in
@@ -189,7 +202,7 @@ let print_record env mind mib =
| Monomorphic_ind _ | Polymorphic_ind _ -> str ""
| Cumulative_ind cumi ->
Printer.pr_cumulativity_info
- sigma (Univ.instantiate_cumulativity_info cumi)
+ sigma (instantiate_cumulativity_info cumi)
)
let pr_mutual_inductive_body env mind mib =
@@ -292,11 +305,13 @@ let print_body is_impl env mp (l,body) =
| SFBmodule _ -> keyword "Module" ++ spc () ++ name
| SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name
| SFBconst cb ->
+ let ctx = Declareops.constant_polymorphic_context cb in
let u =
if Declareops.constant_is_polymorphic cb then
- Declareops.constant_polymorphic_instance cb
+ Univ.AUContext.instance ctx
else Univ.Instance.empty
in
+ let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in
let sigma = Evd.empty in
(match cb.const_body with
| Def _ -> def "Definition" ++ spc ()
@@ -316,8 +331,7 @@ let print_body is_impl env mp (l,body) =
Printer.pr_lconstr_env env sigma
(Vars.subst_instance_constr u (Mod_subst.force_constr l)))
| _ -> mt ()) ++ str "." ++
- Printer.pr_universe_ctx sigma
- (Declareops.constant_polymorphic_context cb))
+ Printer.pr_universe_ctx sigma ctx)
| SFBmind mib ->
try
let env = Option.get env in
diff --git a/printing/printmod.mli b/printing/printmod.mli
index f3079d5b6b..81b5774537 100644
--- a/printing/printmod.mli
+++ b/printing/printmod.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 06:17:23 +0000