From f610068823b33bdc0af752a646df05b98489d7ce Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 11 Jun 2017 06:08:02 +0200 Subject: [proof] Deprecate redundant wrappers. As we would like to reduce the role of proof_global in future versions, we start to deprecate old compatibility aliases in `Pfedit` in favor of the real functions underlying the 8.5 proof engine. We also deprecate a couple of alias types and explicitly mark the few remaining uses of `Pfedit`. --- printing/printer.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'printing') diff --git a/printing/printer.ml b/printing/printer.ml index 3c31dd96bf..d6f0778f75 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -17,7 +17,6 @@ open Nametab open Evd open Proof_type open Refiner -open Pfedit open Constrextern open Ppconstr open Declarations @@ -812,7 +811,7 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = end let pr_nth_open_subgoal n = - let pf = get_pftreestate () in + let pf = Proof_global.give_me_the_proof () in let { it=gls ; sigma=sigma } = Proof.V82.subgoals pf in pr_subgoal n sigma gls -- cgit v1.2.3 From 2253d2eb4f892f932332358be8537fdb5552ef87 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 12 Jun 2017 11:08:12 +0200 Subject: Remove Show Implicit Arguments command. The command has been broken for 15 years. It is basically dead code. Its former behavior can be mimicked with Set Printing Implicit. Show. --- printing/ppvernac.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'printing') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 781af47892..2633cdd6b5 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -561,7 +561,6 @@ open Decl_kinds | GoalUid n -> spc () ++ str n in let pr_showable = function | ShowGoal n -> keyword "Show" ++ pr_goal_reference n - | ShowGoalImplicitly n -> keyword "Show Implicit Arguments" ++ pr_opt int n | ShowProof -> keyword "Show Proof" | ShowNode -> keyword "Show Node" | ShowScript -> keyword "Show Script" -- cgit v1.2.3 From 6cd14bf253f681d0465f8dce1d84a54a4f104d9c Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 12 Jun 2017 11:22:38 +0200 Subject: Remove non-working Show Tree and Show Node commands. --- printing/ppvernac.ml | 2 -- 1 file changed, 2 deletions(-) (limited to 'printing') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 2633cdd6b5..81f41cba13 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -562,11 +562,9 @@ open Decl_kinds let pr_showable = function | ShowGoal n -> keyword "Show" ++ pr_goal_reference n | ShowProof -> keyword "Show Proof" - | ShowNode -> keyword "Show Node" | ShowScript -> keyword "Show Script" | ShowExistentials -> keyword "Show Existentials" | ShowUniverses -> keyword "Show Universes" - | ShowTree -> keyword "Show Tree" | ShowProofNames -> keyword "Show Conjectures" | ShowIntros b -> keyword "Show " ++ (if b then keyword "Intros" else keyword "Intro") | ShowMatch id -> keyword "Show Match " ++ pr_reference id -- cgit v1.2.3 From 3813ba5229cf42597cd30a08e842e0832e5253cb Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 12 Jun 2017 11:25:26 +0200 Subject: Remove Show Thesis command which was never implemented. --- printing/ppvernac.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'printing') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 81f41cba13..9d28bc4f84 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -568,7 +568,6 @@ open Decl_kinds | ShowProofNames -> keyword "Show Conjectures" | ShowIntros b -> keyword "Show " ++ (if b then keyword "Intros" else keyword "Intro") | ShowMatch id -> keyword "Show Match " ++ pr_reference id - | ShowThesis -> keyword "Show Thesis" in return (pr_showable s) | VernacCheckGuard -> -- cgit v1.2.3 From 63896b2443e71e47c016fc9d0709cc22cf24f288 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 12 Jun 2017 12:37:55 +0200 Subject: [lib] Remove obsolete state-management function add_frozen_state AFAICS this function predates modern state-handling; nowadays summaries are stored by the STM and nobody were using this information. --- printing/prettyp.ml | 2 -- 1 file changed, 2 deletions(-) (limited to 'printing') diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 2b21b3f9e8..3ae7da8fc1 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -587,8 +587,6 @@ let gallina_print_library_entry with_values ent = Some (str " >>>>>>> Module " ++ pr_name oname) | (oname,Lib.ClosedModule _) -> Some (str " >>>>>>> Closed Module " ++ pr_name oname) - | (_,Lib.FrozenState _) -> - None let gallina_print_context with_values = let rec prec n = function -- cgit v1.2.3 From d038839a32978548051573286e22462d68d42ee6 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 26 Apr 2016 17:30:30 +0200 Subject: Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t) This string contains the base-10 representation of the number (big endian) Note that some inner parsing stuff still uses bigints, see egramcoq.ml --- printing/ppconstr.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'printing') diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 626464b96f..49eedb767b 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -80,7 +80,7 @@ let tag_var = tag Tag.variable | Any -> true let prec_of_prim_token = function - | Numeral p -> if Bigint.is_pos_or_zero p then lposint else lnegint + | Numeral (_,b) -> if b then lposint else lnegint | String _ -> latom open Notation @@ -231,7 +231,7 @@ let tag_var = tag Tag.variable | ArgVar (loc,s) -> pr_lident (loc,s) let pr_prim_token = function - | Numeral n -> str (Bigint.to_string n) + | Numeral (n,s) -> str (if s then n else "-"^n) | String s -> qs s let pr_evar pr id l = -- cgit v1.2.3 From fd1f420aef96822bed2ce14214c34e41ceda9b4e Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Sat, 1 Apr 2017 17:35:39 +0200 Subject: Using UInfoInd for universes in inductive types It stores both universe constraints and subtyping information for blocks of inductive declarations. At this stage the there is no inference or checking implemented. The subtyping information simply encodes equality of levels for the condition of subtyping. --- printing/printer.ml | 7 +++++++ printing/printer.mli | 1 + printing/printmod.ml | 10 +++++----- 3 files changed, 13 insertions(+), 5 deletions(-) (limited to 'printing') diff --git a/printing/printer.ml b/printing/printer.ml index d6f0778f75..c27a9b009d 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -261,6 +261,13 @@ let pr_universe_ctx sigma c = else mt() +let pr_universe_info_ind sigma uii = + if !Detyping.print_universes && not (Univ.UInfoInd.is_empty uii) then + fnl()++pr_in_comment (fun uii -> v 0 + (Univ.pr_universe_info_ind (Termops.pr_evd_level sigma) uii)) uii + else + mt() + (**********************************************************************) (* Global references *) diff --git a/printing/printer.mli b/printing/printer.mli index 3fce065613..6531036a1f 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -97,6 +97,7 @@ val pr_sort : evar_map -> sorts -> std_ppcmds val pr_polymorphic : bool -> std_ppcmds val pr_universe_instance : evar_map -> Univ.universe_context -> std_ppcmds val pr_universe_ctx : evar_map -> Univ.universe_context -> std_ppcmds +val pr_universe_info_ind : evar_map -> Univ.universe_info_ind -> std_ppcmds (** Printing global references using names as short as possible *) diff --git a/printing/printmod.ml b/printing/printmod.ml index c4affd4acd..7dc47a4a4c 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -89,7 +89,7 @@ let build_ind_type env mip = let print_one_inductive env sigma mib ((_,i) as ind) = let u = if mib.mind_polymorphic then - Univ.UContext.instance mib.mind_universes + Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes) else Univ.Instance.empty in let mip = mib.mind_packets.(i) in let params = Inductive.inductive_paramdecls (mib,u) in @@ -100,7 +100,7 @@ let print_one_inductive env sigma mib ((_,i) as ind) = let envpar = push_rel_context params env in let inst = if mib.mind_polymorphic then - Printer.pr_universe_instance sigma mib.mind_universes + Printer.pr_universe_instance sigma (Univ.UInfoInd.univ_context mib.mind_universes) else mt () in hov 0 ( @@ -124,7 +124,7 @@ let print_mutual_inductive env mind mib = def keyword ++ spc () ++ prlist_with_sep (fun () -> fnl () ++ str" with ") (print_one_inductive env sigma mib) inds ++ - Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes)) + Printer.pr_universe_info_ind sigma (Univ.instantiate_univ_info_ind mib.mind_universes)) let get_fields = let rec prodec_rec l subst c = @@ -142,7 +142,7 @@ let get_fields = let print_record env mind mib = let u = if mib.mind_polymorphic then - Univ.UContext.instance mib.mind_universes + Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes) else Univ.Instance.empty in let mip = mib.mind_packets.(0) in @@ -175,7 +175,7 @@ let print_record env mind mib = (fun (id,b,c) -> pr_id id ++ str (if b then " : " else " := ") ++ Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++ - Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes)) + Printer.pr_universe_info_ind sigma (Univ.instantiate_univ_info_ind mib.mind_universes)) let pr_mutual_inductive_body env mind mib = if mib.mind_record <> None && not !Flags.raw_print then -- cgit v1.2.3 From 9468e4b49bd2f397b5e1bd2b7994cc84929fb6ac Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 27 Apr 2017 20:16:35 +0200 Subject: Fix bugs and add an option for cumulativity --- printing/ppvernac.ml | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) (limited to 'printing') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 9d28bc4f84..6a47c308d3 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -727,7 +727,7 @@ open Decl_kinds 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 ++ pr_non_empty_arg pr_assumption_inline t ++ spc() ++ assumptions)) - | VernacInductive (p,f,l) -> + | VernacInductive (cum, p,f,l) -> let pr_constructor (coe,(id,c)) = hov 2 (pr_lident id ++ str" " ++ (if coe then str":>" else str":") ++ @@ -754,13 +754,17 @@ open Decl_kinds in let key = let (_,_,_,k,_),_ = List.hd l in - match k with Record -> "Record" | Structure -> "Structure" - | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive" - | Class _ -> "Class" | Variant -> "Variant" + let kind = + match k with Record -> "Record" | Structure -> "Structure" + | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive" + | Class _ -> "Class" | Variant -> "Variant" + in + let cm = if cum then "Cumulative" else "NonCumulative" in + cm ^ " " ^ kind in return ( hov 1 (pr_oneind key (List.hd l)) ++ - (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l)) + (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l)) ) | VernacFixpoint (local, recs) -> -- cgit v1.2.3 From 0c94de1f8c598c1869f71fee86bdbe4f0000a502 Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 4 May 2017 19:12:45 +0200 Subject: Add printing of cumulativity in inductive types --- printing/ppvernac.ml | 6 ++++-- printing/printer.ml | 5 +++++ printing/printer.mli | 1 + printing/printmod.ml | 10 ++++++---- 4 files changed, 16 insertions(+), 6 deletions(-) (limited to 'printing') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 6a47c308d3..4a5cfe6301 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -759,8 +759,10 @@ open Decl_kinds | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive" | Class _ -> "Class" | Variant -> "Variant" in - let cm = if cum then "Cumulative" else "NonCumulative" in - cm ^ " " ^ kind + if p then + let cm = if cum then "Cumulative" else "NonCumulative" in + cm ^ " " ^ kind + else kind in return ( hov 1 (pr_oneind key (List.hd l)) ++ diff --git a/printing/printer.ml b/printing/printer.ml index c27a9b009d..1d7b7cff0f 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -998,6 +998,11 @@ let pr_assumptionset env s = let xor a b = (a && not b) || (not a && b) +let pr_cumulative p b = + if p then + if b then str "Cumulative " else str "NonCumulative " + else str "" + let pr_polymorphic b = let print = xor (Flags.is_universe_polymorphism ()) b in if print then diff --git a/printing/printer.mli b/printing/printer.mli index 6531036a1f..9f4ea23b74 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -95,6 +95,7 @@ val pr_sort : evar_map -> sorts -> std_ppcmds (** Universe constraints *) val pr_polymorphic : bool -> std_ppcmds +val pr_cumulative : bool -> bool -> std_ppcmds val pr_universe_instance : evar_map -> Univ.universe_context -> std_ppcmds val pr_universe_ctx : evar_map -> Univ.universe_context -> std_ppcmds val pr_universe_info_ind : evar_map -> Univ.universe_info_ind -> std_ppcmds diff --git a/printing/printmod.ml b/printing/printmod.ml index 7dc47a4a4c..be8940b6ff 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -121,10 +121,11 @@ let print_mutual_inductive env mind mib = let bl = Universes.universe_binders_of_global (IndRef (mind, 0)) in let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in hov 0 (Printer.pr_polymorphic mib.mind_polymorphic ++ - def keyword ++ spc () ++ - prlist_with_sep (fun () -> fnl () ++ str" with ") - (print_one_inductive env sigma mib) inds ++ - Printer.pr_universe_info_ind sigma (Univ.instantiate_univ_info_ind mib.mind_universes)) + Printer.pr_cumulative mib.mind_polymorphic mib.mind_cumulative ++ + def keyword ++ spc () ++ + prlist_with_sep (fun () -> fnl () ++ str" with ") + (print_one_inductive env sigma mib) inds ++ + Printer.pr_universe_info_ind sigma (Univ.instantiate_univ_info_ind mib.mind_universes)) let get_fields = let rec prodec_rec l subst c = @@ -165,6 +166,7 @@ let print_record env mind mib = hov 0 ( hov 0 ( Printer.pr_polymorphic mib.mind_polymorphic ++ + Printer.pr_cumulative mib.mind_polymorphic mib.mind_cumulative ++ def keyword ++ spc () ++ pr_id mip.mind_typename ++ brk(1,4) ++ print_params env sigma params ++ str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ brk(1,2) ++ -- cgit v1.2.3 From ff918e4bb0ae23566e038f4b55d84dd2c343f95e Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 1 Jun 2017 16:18:19 +0200 Subject: Clean up universes of constants and inductives --- printing/prettyp.ml | 10 ++++------ printing/printer.ml | 17 +++++++++-------- printing/printer.mli | 2 +- printing/printmod.ml | 43 +++++++++++++++++++++++++++++-------------- 4 files changed, 43 insertions(+), 29 deletions(-) (limited to 'printing') diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 3ae7da8fc1..6d2bf6b73a 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -502,8 +502,8 @@ let ungeneralized_type_of_constant_type t = Typeops.type_of_constant_type (Global.env ()) t let print_instance sigma cb = - if cb.const_polymorphic then - pr_universe_instance sigma cb.const_universes + if Declareops.constant_is_polymorphic cb then + pr_universe_instance sigma (Declareops.constant_polymorphic_context cb) else mt() let print_constant with_values sep sp = @@ -511,16 +511,14 @@ let print_constant with_values sep sp = let val_0 = Global.body_of_constant_body cb in let typ = Declareops.type_of_constant cb in let typ = ungeneralized_type_of_constant_type typ in - let univs = Univ.instantiate_univ_context - (Global.universes_of_constant_body cb) - in + let univs = Global.universes_of_constant_body cb in let ctx = Evd.evar_universe_context_of_binders (Universes.universe_binders_of_global (ConstRef sp)) in let env = Global.env () and sigma = Evd.from_ctx ctx in let pr_ltype = pr_ltype_env env sigma in - hov 0 (pr_polymorphic cb.const_polymorphic ++ + hov 0 (pr_polymorphic (Declareops.constant_is_polymorphic cb) ++ match val_0 with | None -> str"*** [ " ++ diff --git a/printing/printer.ml b/printing/printer.ml index 1d7b7cff0f..3b0b6d5d23 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -261,10 +261,11 @@ let pr_universe_ctx sigma c = else mt() -let pr_universe_info_ind sigma uii = - if !Detyping.print_universes && not (Univ.UInfoInd.is_empty uii) then - fnl()++pr_in_comment (fun uii -> v 0 - (Univ.pr_universe_info_ind (Termops.pr_evd_level sigma) uii)) uii +let pr_cumulativity_info sigma cumi = + if !Detyping.print_universes + && not (Univ.UContext.is_empty (Univ.CumulativityInfo.univ_context cumi)) then + fnl()++pr_in_comment (fun uii -> v 0 + (Univ.pr_cumulativity_info (Termops.pr_evd_level sigma) uii)) cumi else mt() @@ -998,10 +999,10 @@ let pr_assumptionset env s = let xor a b = (a && not b) || (not a && b) -let pr_cumulative p b = - if p then - if b then str "Cumulative " else str "NonCumulative " - else str "" +let pr_cumulative poly cum = + if poly then + if cum then str "Cumulative " else str "NonCumulative " + else mt () let pr_polymorphic b = let print = xor (Flags.is_universe_polymorphism ()) b in diff --git a/printing/printer.mli b/printing/printer.mli index 9f4ea23b74..f0a32bbbdf 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -98,7 +98,7 @@ val pr_polymorphic : bool -> std_ppcmds val pr_cumulative : bool -> bool -> std_ppcmds val pr_universe_instance : evar_map -> Univ.universe_context -> std_ppcmds val pr_universe_ctx : evar_map -> Univ.universe_context -> std_ppcmds -val pr_universe_info_ind : evar_map -> Univ.universe_info_ind -> std_ppcmds +val pr_cumulativity_info : evar_map -> Univ.cumulativity_info -> std_ppcmds (** Printing global references using names as short as possible *) diff --git a/printing/printmod.ml b/printing/printmod.ml index be8940b6ff..08d177f53e 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -88,8 +88,8 @@ let build_ind_type env mip = Inductive.type_of_inductive env mip let print_one_inductive env sigma mib ((_,i) as ind) = - let u = if mib.mind_polymorphic then - Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes) + let u = if Declareops.inductive_is_polymorphic mib then + Declareops.inductive_polymorphic_instance mib else Univ.Instance.empty in let mip = mib.mind_packets.(i) in let params = Inductive.inductive_paramdecls (mib,u) in @@ -99,8 +99,8 @@ let print_one_inductive env sigma mib ((_,i) as ind) = let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in let envpar = push_rel_context params env in let inst = - if mib.mind_polymorphic then - Printer.pr_universe_instance sigma (Univ.UInfoInd.univ_context mib.mind_universes) + if Declareops.inductive_is_polymorphic mib then + Printer.pr_universe_instance sigma (Declareops.inductive_polymorphic_context mib) else mt () in hov 0 ( @@ -120,12 +120,18 @@ let print_mutual_inductive env mind mib = in let bl = Universes.universe_binders_of_global (IndRef (mind, 0)) in let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in - hov 0 (Printer.pr_polymorphic mib.mind_polymorphic ++ - Printer.pr_cumulative mib.mind_polymorphic mib.mind_cumulative ++ + hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++ + Printer.pr_cumulative + (Declareops.inductive_is_polymorphic mib) + (Declareops.inductive_is_cumulative mib) ++ def keyword ++ spc () ++ prlist_with_sep (fun () -> fnl () ++ str" with ") (print_one_inductive env sigma mib) inds ++ - Printer.pr_universe_info_ind sigma (Univ.instantiate_univ_info_ind mib.mind_universes)) + match mib.mind_universes with + | Monomorphic_ind _ | Polymorphic_ind _ -> str "" + | Cumulative_ind cumi -> + Printer.pr_cumulativity_info + sigma (Univ.instantiate_cumulativity_info cumi)) let get_fields = let rec prodec_rec l subst c = @@ -142,8 +148,8 @@ let get_fields = let print_record env mind mib = let u = - if mib.mind_polymorphic then - Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes) + if Declareops.inductive_is_polymorphic mib then + Declareops.inductive_polymorphic_instance mib else Univ.Instance.empty in let mip = mib.mind_packets.(0) in @@ -165,8 +171,10 @@ let print_record env mind mib = in hov 0 ( hov 0 ( - Printer.pr_polymorphic mib.mind_polymorphic ++ - Printer.pr_cumulative mib.mind_polymorphic mib.mind_cumulative ++ + Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++ + Printer.pr_cumulative + (Declareops.inductive_is_polymorphic mib) + (Declareops.inductive_is_cumulative mib) ++ def keyword ++ spc () ++ pr_id mip.mind_typename ++ brk(1,4) ++ print_params env sigma params ++ str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ brk(1,2) ++ @@ -177,7 +185,12 @@ let print_record env mind mib = (fun (id,b,c) -> pr_id id ++ str (if b then " : " else " := ") ++ Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++ - Printer.pr_universe_info_ind sigma (Univ.instantiate_univ_info_ind mib.mind_universes)) + match mib.mind_universes with + | Monomorphic_ind _ | Polymorphic_ind _ -> str "" + | Cumulative_ind cumi -> + Printer.pr_cumulativity_info + sigma (Univ.instantiate_cumulativity_info cumi) + ) let pr_mutual_inductive_body env mind mib = if mib.mind_record <> None && not !Flags.raw_print then @@ -280,7 +293,8 @@ let print_body is_impl env mp (l,body) = | SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name | SFBconst cb -> let u = - if cb.const_polymorphic then Univ.UContext.instance cb.const_universes + if Declareops.constant_is_polymorphic cb then + Declareops.constant_polymorphic_instance cb else Univ.Instance.empty in let sigma = Evd.empty in @@ -302,7 +316,8 @@ 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 (Univ.instantiate_univ_context cb.const_universes)) + Printer.pr_universe_ctx sigma + (Declareops.constant_polymorphic_context cb)) | SFBmind mib -> try let env = Option.get env in -- cgit v1.2.3 From 94e0cbc26718fe3fecc58f6f8673f5f8abb0ce31 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 21 Jun 2017 15:12:21 +0200 Subject: [vernac] Remove stale bool parameter from `VernacStartTheoremProof` `VernacStartTheoremProof` contained a stale bool parameter from 15 years ago, which is unused today. --- printing/ppvernac.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'printing') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 4a5cfe6301..d0536a1744 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -698,7 +698,7 @@ open Decl_kinds | Some cc -> str" :=" ++ spc() ++ cc)) ) - | VernacStartTheoremProof (ki,l,_) -> + | VernacStartTheoremProof (ki,l) -> return ( hov 1 (pr_statement (pr_thm_token ki) (List.hd l) ++ prlist (pr_statement (spc () ++ keyword "with")) (List.tl l)) -- cgit v1.2.3