Simplification: cumulativity information is variance information.

Since cumulativity of an inductive type is the universe constraints
which make a term convertible with its universe-renamed copy, the only
constraints we can get are between a universe and its copy.

As such we do not need to be able to represent arbitrary constraints
between universes and copied universes in a double-sized ucontext,
instead we can just keep around an array describing whether a bound
universe is covariant, invariant or irrelevant (CIC has no
contravariant conversion rule).

Printing is fairly obtuse and should be improved: when we print the
CumulativityInfo we add marks to the universes of the instance: = for
invariant, + for covariant and * for irrelevant. ie

         Record Foo@{i j k} := { foo : Type@{i} -> Type@{j} }.
         Print Foo.

gives

        Cumulative Record Foo : Type@{max(i+1, j+1)} := Build_Foo
          { foo : Type@{i} -> Type@{j} }
          (* =i +j *k |=  *)

1 files changed, 1 insertions, 2 deletions

diff --git a/printing/printmod.ml b/printing/printmod.ml
index fb9d45a79..35487e09c 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))