Move to a representation of universe polymorphic constants using indices for variables.

Simplifies instantiation of constants/inductives, requiring less allocation and Map.find's.
Abstraction by variables is handled mostly inside the kernel but could be moved outside.

1 files changed, 9 insertions, 7 deletions

diff --git a/printing/printer.ml b/printing/printer.ml
index 03f416a510..55a7d36a3c 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -756,12 +756,12 @@ let build_ind_type env mip =
   Inductive.type_of_inductive env mip
 
 let print_one_inductive env mib ((_,i) as ind) =
-  let mip = mib.mind_packets.(i) in
-  let params = mib.mind_params_ctxt in
-  let args = extended_rel_list 0 params in
   let u = if mib.mind_polymorphic then 
       Univ.UContext.instance mib.mind_universes 
     else Univ.Instance.empty in
+  let mip = mib.mind_packets.(i) in
+  let params = Inductive.inductive_paramdecls (mib,u) in
+  let args = extended_rel_list 0 params in
   let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in
   let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in
   let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in
@@ -794,12 +794,14 @@ let get_fields =
   prodec_rec [] []
 
 let print_record env mind mib =
+  let u = 
+    if mib.mind_polymorphic then 
+      Univ.UContext.instance mib.mind_universes 
+    else Univ.Instance.empty 
+  in
   let mip = mib.mind_packets.(0) in
-  let params = mib.mind_params_ctxt in
+  let params = Inductive.inductive_paramdecls (mib,u) in
   let args = extended_rel_list 0 params in
-  let u = if mib.mind_polymorphic then 
-      Univ.UContext.instance mib.mind_universes 
-    else Univ.Instance.empty in
   let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in
   let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (mib,mip) in
   let cstrtype = hnf_prod_applist env cstrtypes.(0) args in