diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-07-17 07:47:31 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-07-17 07:47:31 +0200 |
| commit | 3a5dd0df47b83a1a46061f2a14761d3d9ad79fcb (patch) | |
| tree | 843408d6fa6a37307c0441d7fa81b3df6ae277e2 /printing/printmod.ml | |
| parent | 0c297ad43bd4b0b8187aa56756334bd294a212ca (diff) | |
| parent | b21cd4620e0983a23dd11c0f582bf367662aeee3 (diff) | |
Merge PR #878: Prepare De Bruijn universe abstractions, Episode II: Upper layers
Diffstat (limited to 'printing/printmod.ml')
| -rw-r--r-- | printing/printmod.ml | 15 |
1 files changed, 13 insertions, 2 deletions
diff --git a/printing/printmod.ml b/printing/printmod.ml index 2e0e6d284..5c7dcdc10 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -110,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 @@ -133,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 = @@ -191,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 = |