Adapt to PR#18903

examples/HoTT_light.v

@@ -268,8 +268,8 @@ Proof. reduce. destruct X. destruct X0. destruct x0. reflexivity. Defined.
 
 Definition trans_co_eq_inv_arrow_morphism@{i j k} :
   ∀ (A : Type@{i}) (R : crelation@{i j} A),
-    Transitive R → Proper@{k j} (respectful@{i j k j k j} R
-    (respectful@{i j k j k j} Id (@flip@{k k k} _ _ Type@{j} arrow))) R.
+    Transitive R → Proper@{k j} (respectful@{i j k j} R
+    (respectful@{i j k j} Id (@flip@{k k k} _ _ Type@{j} arrow))) R.
 Proof. reduce. transitivity y. assumption. now destruct X1. Defined.
 #[local] Existing Instance trans_co_eq_inv_arrow_morphism.
 
@@ -458,7 +458,7 @@ Definition path_contr {A} {H:Contr A} (x y : A) : x = y
 Definition path2_contr {A} {H:Contr A} {x y : A} (p q : x = y) : p = q.
   assert (K : forall (r : x = y), r = path_contr x y).
   intro r; destruct r; symmetry; now apply concat_Vp.
-  apply (transitivity (y:=path_contr x y)).
+  apply (transitivity (path_contr x y)).
   - apply K.
   - symmetry; apply K.
 Defined.

src/equations_common.ml

@@ -221,13 +221,14 @@ let e_type_of env evd t =
   evd := evm; t
 
 let collapse_term_qualities uctx c =
-  let nf_evar _ = None in
-  let nf_qvar q = match UState.nf_qvar uctx q with
-    | QConstant _ as q -> q
-    | QVar q -> (* hack *) QConstant QType
-  in
-  let nf_univ _ = None in
-  UnivSubst.nf_evars_and_universes_opt_subst nf_evar nf_qvar nf_univ c
+  let rec self () c =
+    let nf_qvar q = match UState.nf_qvar uctx q with
+      | QConstant _ as q -> q
+      | QVar q -> (* hack *) QConstant QType
+    in
+    let nf_univ _ = None in
+    UnivSubst.map_universes_opt_subst_with_binders id self nf_qvar nf_univ () c
+  in self () c
 
 let make_definition ?opaque ?(poly=false) evm ?types b =
   let env = Global.env () in
@@ -257,7 +258,7 @@ let declare_constant id body ty ~poly ~kind evd =
   let cst = Declare.declare_constant ~name:id (Declare.DefinitionEntry ce) ~kind in
   Flags.if_verbose Feedback.msg_info (str((Id.to_string id) ^ " is defined"));
   if poly then
-    let cstr = EConstr.(mkConstU (cst, EInstance.make (UVars.UContext.instance (Evd.to_universe_context evm)))) in
+    let cstr = EConstr.(mkConstU (cst, EInstance.make (UVars.Instance.of_level_instance (UVars.UContext.instance (Evd.to_universe_context evm))))) in
     cst, (evm0, cstr)
   else cst, (evm0, EConstr.UnsafeMonomorphic.mkConst cst)
 
@@ -1101,20 +1102,9 @@ let evd_comb1 f evd x =
 let nonalgebraic_universe_level_of_universe env sigma u =
   match ESorts.kind sigma u with
   | Sorts.Set | Sorts.Prop | Sorts.SProp ->
-    sigma, Univ.Level.set, u
-  | Sorts.Type u0 | Sorts.QSort (_, u0) ->
-    match Univ.Universe.level u0 with
-    | Some l ->
-      (match Evd.universe_rigidity sigma l with
-      | Evd.UnivFlexible true ->
-        Evd.make_nonalgebraic_variable sigma l, l, ESorts.make @@ Sorts.sort_of_univ @@ Univ.Universe.make l
-      | _ -> sigma, l, u)
-    | None ->
-      let sigma, l = Evd.new_univ_level_variable Evd.univ_flexible sigma in
-      let ul = ESorts.make @@ Sorts.sort_of_univ @@ Univ.Universe.make l in
-      let sigma = Evd.set_leq_sort env sigma u ul in
-      sigma, l, ul
-
+    sigma, Univ.Universe.type0, u
+  | Sorts.Type u0 | Sorts.QSort (_, u0) -> sigma, u0, u
+
 let instance_of env sigma ?argu goalu =
   let sigma, goall, goalu = nonalgebraic_universe_level_of_universe env sigma goalu in
   let inst =

src/equations_common.mli

@@ -442,7 +442,7 @@ val splay_prod_n_assum : env -> Evd.evar_map -> int -> types -> rel_context * ty
 
 (* Universes *)
 val nonalgebraic_universe_level_of_universe :
-  Environ.env -> Evd.evar_map -> ESorts.t -> Evd.evar_map * Univ.Level.t * ESorts.t
+  Environ.env -> Evd.evar_map -> ESorts.t -> Evd.evar_map * Univ.Universe.t * ESorts.t
 val instance_of :
   Environ.env ->
   Evd.evar_map ->

src/noconf.ml

@@ -138,12 +138,7 @@ let derive_no_confusion ~pm env sigma0 ~poly (ind,u as indu) =
   let id = add_prefix "NoConfusion_" indid in
   let cstNoConf = Declare.declare_constant ~name:id (Declare.DefinitionEntry ce) ~kind:Decls.(IsDefinition Definition) in
   let env = Global.env () in
-  let sigma = Evd.from_env env in
-  let sigma, indu = Evd.fresh_global
-      ~rigid:Evd.univ_rigid (* Universe levels of the inductive family should not be tampered with. *)
-      env sigma (GlobRef.IndRef ind) in
-  let indu = destInd sigma indu in
-  Noconf_hom.derive_noConfusion_package ~pm env sigma ~poly indu indid
+  Noconf_hom.derive_noConfusion_package ~pm env ~poly ind indid
     ~prefix:"" ~tactic:(noconf_tac ()) cstNoConf
 
 let () =

src/noconf_hom.ml

@@ -53,21 +53,21 @@ let get_forced_positions sigma args concl =
   in
   List.rev (List.fold_left_i is_forced 1 [] args)
 
-let derive_noConfusion_package ~pm env sigma ~poly (ind,u as indu) indid ~prefix ~tactic cstNoConf =
+let derive_noConfusion_package ~pm env ~poly ind indid ~prefix ~tactic cstNoConf =
+  let sigma = Evd.from_env env in
+  let noid = add_prefix "noConfusion" (add_prefix prefix (add_prefix "_" indid))
+  and packid = add_prefix "NoConfusion" (add_prefix prefix (add_prefix "Package_" indid)) in
+  let tc = Typeclasses.class_info_exn env sigma (Lazy.force coq_noconfusion_class) in
+  let sigma, noconf = Evd.fresh_global ~rigid:Evd.univ_rigid env sigma (GlobRef.ConstRef cstNoConf) in
+  let sigma, noconfcl = new_global sigma tc.Typeclasses.cl_impl in
+  let inst, u = destInd sigma noconfcl in
   let mindb, oneind = Global.lookup_inductive ind in
   let ctx = List.map of_rel_decl oneind.mind_arity_ctxt in
-  let ctx = subst_instance_context (snd indu) ctx in
   let ctx = smash_rel_context ctx in
   let len =
     if prefix = "" then mindb.mind_nparams
     else List.length ctx in
   let argsvect = rel_vect 0 len in
-  let noid = add_prefix "noConfusion" (add_prefix prefix (add_prefix "_" indid))
-  and packid = add_prefix "NoConfusion" (add_prefix prefix (add_prefix "Package_" indid)) in
-  let tc = Typeclasses.class_info_exn env sigma (Lazy.force coq_noconfusion_class) in
-  let sigma, noconf = Evd.fresh_global ~rigid:Evd.univ_rigid env sigma (GlobRef.ConstRef cstNoConf) in
-  let sigma, noconfcl = new_global sigma tc.Typeclasses.cl_impl in
-  let inst, u = destInd sigma noconfcl in
   let noconfterm = mkApp (noconf, argsvect) in
   let ctx, argty =
     let ty = Retyping.get_type_of env sigma noconf in
@@ -267,12 +267,7 @@ let derive_no_confusion_hom ~pm env sigma0 ~poly (ind,u as indu) =
     (* The principles are now shown, let's prove this forms an equivalence *)
     Global.set_strategy (Conv_oracle.EvalConstRef program_cst) Conv_oracle.transparent;
     let env = Global.env () in
-    let sigma = Evd.from_env env in
-    let sigma, indu = Evd.fresh_global
-        ~rigid:Evd.univ_rigid (* Universe levels of the inductive family should not be tampered with. *)
-        env sigma (GlobRef.IndRef ind) in
-    let indu = destInd sigma indu in
-    (), derive_noConfusion_package ~pm env sigma ~poly indu indid
+    (), derive_noConfusion_package ~pm env ~poly ind indid
       ~prefix:"Hom" ~tactic:(noconf_hom_tac ()) program_cst
  in
  let prog = Splitting.make_single_program env evd data.Covering.flags p ctxmap splitting None in

src/noconf_hom.mli

@@ -12,9 +12,8 @@ open EConstr
 val derive_noConfusion_package :
   pm:Declare.OblState.t ->
   Environ.env ->
-  Evd.evar_map ->
   poly:bool ->
-  Names.inductive * EConstr.EInstance.t ->
+  Names.inductive ->
   Names.Id.t ->
   prefix:string ->
   tactic:unit Proofview.tactic ->

src/sigma_types.ml

@@ -139,7 +139,7 @@ let telescope env evd = function
             let sigty = mkAppG env evd (Lazy.force coq_sigma) [|t; pred|] in
             let _, u = destInd !evd (fst (destApp !evd sigty)) in
             let _, ua = UVars.Instance.to_array (EInstance.kind !evd u) in
-            let l = Sorts.sort_of_univ @@ Univ.Universe.make ua.(0) in
+            let l = Sorts.sort_of_univ @@ ua.(0) in
             (* Ensure that the universe of the sigma is only >= those of t and pred *)
             let open UnivProblem in
             let enforce_leq env sigma t cstr =

src/splitting.ml

@@ -1114,9 +1114,10 @@ let gather_fresh_context sigma u octx =
       Sorts.QVar.Set.empty qarr
   in
   let levels =
-    Array.fold_left (fun ctx' l ->
-        if not (Univ.Level.Set.mem l univs) then Univ.Level.Set.add l ctx'
-        else ctx')
+    Array.fold_left (fun ctx' u ->
+      let levels = Univ.Universe.levels u in
+      let levels = Univ.Level.Set.diff levels univs in
+      Univ.Level.Set.union levels ctx')
       Univ.Level.Set.empty uarr
   in
   (qualities, levels), (UVars.AbstractContext.instantiate u octx)

test-suite/LogicType.v

@@ -41,25 +41,28 @@ Require Import Equations.Type.FunctionalInduction.
 
 Set Universe Minimization ToSet.
 Derive NoConfusionHom for vector.
+
+Print NoConfusionHomPackage_vector.
 Unset Universe Minimization ToSet.
 
 #[export]
-Instance vector_eqdec@{i +|+} {A : Type@{i}} {n} `(EqDec@{i} A) : EqDec (vector A n).
+Instance vector_eqdec@{i} {A : Type@{i}} {n} `(EqDec@{i} A) : EqDec@{i} (vector@{i} A n).
 Proof.
   intros. intros x. intros y. induction x.
   - left. now depelim y.
   - depelim y.
     pose proof (Classes.eq_dec a a0).
     dependent elimination X as [inl id_refl|inr Ha].
-    -- specialize (IHx v).
-       dependent elimination IHx as [inl id_refl|inr H'].
-       --- left; reflexivity.
-       --- right. simplify *. now apply H'.
+    -- specialize (IHx v). 
+        dependent elimination IHx as [inl id_refl|inr H'].
+        --- left; reflexivity.
+        --- right. simplify *. now apply H'.
     -- right; simplify *. now apply Ha.
 Defined.
 
 Record vect {A} := mkVect { vect_len : nat; vect_vector : vector A vect_len }.
 Coercion mkVect : vector >-> vect.
+Set Universe Minimization ToSet.
 
 Derive NoConfusion for vect.
 Reserved Notation "x ++v y" (at level 60).
@@ -98,7 +101,7 @@ Section foo.
     | (xs, ys) := (cons x xs, cons y ys) }.
 End foo.
 
-
+Set Universe Minimization ToSet.
 Section vlast.
   Context {A : Type}.
   Equations vlast {n} (v : vector A (S n)) : A by wf (signature_pack v) (@vector_subterm A) :=

theories/Prop/DepElim.v

@@ -125,7 +125,7 @@ Proof.
   intros X. eapply (X eq_refl). apply eq_refl.
 Defined.
 
-Polymorphic Lemma eq_simplification_sigma1_dep@{i j | i <= eq.u0 +} {A : Type@{i}} {P : A -> Type@{i}} {B : Type@{j}}
+Polymorphic Lemma eq_simplification_sigma1_dep@{i j | i <= eq.u0 ?} {A : Type@{i}} {P : A -> Type@{i}} {B : Type@{j}}
   (p q : A) (x : P p) (y : P q) :
   (forall e : p = q, (@eq_rect A p P x q e) = y -> B) ->
   ((p, x) = (q, y) -> B).
@@ -158,11 +158,11 @@ Proof.
   apply (X eq_refl eq_refl).
 Defined.
 
-Polymorphic Definition pack_sigma_eq@{i | +} {A : Type@{i}} {P : A -> Type@{i}} {p q : A} {x : P p} {y : P q}
+Polymorphic Definition pack_sigma_eq@{i | ?} {A : Type@{i}} {P : A -> Type@{i}} {p q : A} {x : P p} {y : P q}
   (e' : p = q) (e : @eq_rect A p P x q e' = y) : (p, x) = (q, y).
 Proof. destruct e'. simpl in e. destruct e. apply eq_refl. Defined.
 
-Polymorphic Lemma eq_simplification_sigma1_dep_dep@{i j | i <= eq.u0 +} {A : Type@{i}} {P : A -> Type@{i}}
+Polymorphic Lemma eq_simplification_sigma1_dep_dep@{i j | i <= eq.u0 ?} {A : Type@{i}} {P : A -> Type@{i}}
   (p q : A) (x : P p) (y : P q) {B : (p, x) = (q, y) -> Type@{j}} :
   (forall e' : p = q, forall e : @eq_rect A p P x q e' = y, B (pack_sigma_eq e' e)) ->
   (forall e : (p, x) = (q, y), B e).
@@ -177,20 +177,20 @@ Proof.
   apply (X eq_refl eq_refl).
 Defined.
 Set Printing Universes.
-Polymorphic Lemma pr2_inv_uip@{i| i <= eq.u0 +} {A : Type@{i}}
+Polymorphic Lemma pr2_inv_uip@{i| i <= eq.u0 ?} {A : Type@{i}}
             {P : A -> Type@{i}} {x : A} {y y' : P x} :
   y = y' -> sigmaI@{i} P x y = sigmaI@{i} P x y'.
 Proof. exact (solution_right (P:=fun y' => (x, y) = (x, y')) y eq_refl y'). Defined.
 
-Polymorphic Lemma pr2_uip@{i | +} {A : Type@{i}}
+Polymorphic Lemma pr2_uip@{i | ?} {A : Type@{i}}
             {E : UIP A} {P : A -> Type@{i}} {x : A} {y y' : P x} :
   sigmaI@{i} P x y = sigmaI@{i} P x y' -> y = y'.
 Proof.
   refine (eq_simplification_sigma1_dep_dep@{i i} _ _ _ _ _).
   intros e'. destruct (uip eq_refl e'). intros e ; exact e.
 Defined.
 
-Polymorphic Lemma pr2_uip_refl@{i | +} {A : Type@{i}}
+Polymorphic Lemma pr2_uip_refl@{i | ?} {A : Type@{i}}
             {E : UIP A} (P : A -> Type@{i}) (x : A) (y : P x) :
   pr2_uip@{i} (@eq_refl _ (x, y)) = eq_refl.
 Proof.
@@ -201,13 +201,13 @@ Defined.
 (** If we have decidable equality on [A] we use this version which is 
    axiom-free! *)
 
-Polymorphic Lemma simplification_sigma2_uip@{i j |+} :
+Polymorphic Lemma simplification_sigma2_uip@{i j |?} :
   forall {A : Type@{i}} `{UIP A} {P : A -> Type@{i}} {B : Type@{j}}
     (p : A) (x y : P p),
     (x = y -> B) -> ((p , x) = (p, y) -> B).
 Proof. intros. apply X. apply pr2_uip@{i} in H0. assumption. Defined.
 
-Polymorphic Lemma simplification_sigma2_uip_refl@{i j | +} :
+Polymorphic Lemma simplification_sigma2_uip_refl@{i j | ?} :
   forall {A : Type@{i}} {uip:UIP A} {P : A -> Type@{i}} {B : Type@{j}}
     (p : A) (x : P p) (G : x = x -> B),
       @simplification_sigma2_uip A uip P B p x x G eq_refl = G eq_refl.
@@ -223,7 +223,7 @@ Polymorphic Lemma simplification_sigma2_dec_point :
     (x = y -> B) -> ((p, x) = (p, y) -> B).
 Proof. intros. apply X. apply inj_right_sigma_point in H0. assumption. Defined.
 
-Polymorphic Lemma simplification_sigma2_dec_point_refl@{i +} :
+Polymorphic Lemma simplification_sigma2_dec_point_refl@{i ?} :
   forall {A} (p : A) `{eqdec:EqDecPoint A p} {P : A -> Type} {B}
     (x : P p) (G : x = x -> B),
       @simplification_sigma2_dec_point A p eqdec P B x x G eq_refl = G eq_refl.
@@ -233,7 +233,7 @@ Proof.
 Defined.
 Arguments simplification_sigma2_dec_point : simpl never.
 
-Polymorphic Lemma simplification_K_uip@{i j| i <= eq.u0 +} {A : Type@{i}} `{UIP A} (x : A) {B : x = x -> Type@{j}} :
+Polymorphic Lemma simplification_K_uip@{i j| i <= eq.u0 ?} {A : Type@{i}} `{UIP A} (x : A) {B : x = x -> Type@{j}} :
   B eq_refl -> (forall p : x = x, B p).
 Proof. apply UIP_K. Defined.
 Arguments simplification_K_uip : simpl never.
@@ -247,7 +247,7 @@ Proof.
 Defined.
 
 Polymorphic
-Definition ind_pack_eq@{i | +} {A : Type@{i}} {B : A -> Type@{i}} {x : A} {p q : B x} (e : p = q) :
+Definition ind_pack_eq@{i | ?} {A : Type@{i}} {B : A -> Type@{i}} {x : A} {p q : B x} (e : p = q) :
   @eq (sigma (fun x => B x)) (x, p) (x, q) :=
   (pr2_inv_uip e).
 
@@ -268,7 +268,7 @@ Arguments pr2_uip : simpl never.
 Arguments pr2_inv_uip : simpl never.
 
 Polymorphic
-Lemma simplify_ind_pack@{i j | +} {A : Type@{i}} {uip : UIP A}
+Lemma simplify_ind_pack@{i j | ?} {A : Type@{i}} {uip : UIP A}
       (B : A -> Type@{i}) (x : A) (p q : B x) (G : p = q -> Type@{j}) :
       (forall e : (x, p) = (x, q), opaque_ind_pack_eq_inv G e) ->
   (forall e : p = q, G e).
@@ -280,7 +280,7 @@ Defined.
 Arguments simplify_ind_pack : simpl never.
 
 Polymorphic
-Lemma simplify_ind_pack_inv@{i j | +} {A : Type@{i}} {uip : UIP A}
+Lemma simplify_ind_pack_inv@{i j | ?} {A : Type@{i}} {uip : UIP A}
       (B : A -> Type@{i}) (x : A) (p : B x) (G : p = p -> Type@{j}) :
   G eq_refl -> opaque_ind_pack_eq_inv G eq_refl.
 Proof.
@@ -289,22 +289,22 @@ Defined.
 Arguments simplify_ind_pack_inv : simpl never.
 
 Polymorphic
-Definition simplified_ind_pack@{i j | +} {A : Type@{i}} {uip : UIP A}
+Definition simplified_ind_pack@{i j | ?} {A : Type@{i}} {uip : UIP A}
   (B : A -> Type@{i}) (x : A) (p : B x) (G : p = p -> Type@{j})
   (t : opaque_ind_pack_eq_inv G eq_refl) :=
   eq_rect _ G t _ (@pr2_uip_refl A uip B x p).
 Arguments simplified_ind_pack : simpl never.
 
 Polymorphic
-Lemma simplify_ind_pack_refl@{i j | +} {A : Type@{i}} {uip : UIP A}
+Lemma simplify_ind_pack_refl@{i j | ?} {A : Type@{i}} {uip : UIP A}
 (B : A -> Type@{i}) (x : A) (p : B x) (G : p = p -> Type@{j})
 (t : forall (e : (x, p) = (x, p)), opaque_ind_pack_eq_inv G e) :
   simplify_ind_pack B x p p G t eq_refl =
   simplified_ind_pack B x p G (t eq_refl).
 Proof. reflexivity. Qed.
 
 Polymorphic
-Lemma simplify_ind_pack_elim@{i j | +} {A : Type@{i}} {uip : UIP A}
+Lemma simplify_ind_pack_elim@{i j | ?} {A : Type@{i}} {uip : UIP A}
   (B : A -> Type@{i}) (x : A) (p : B x) (G : p = p -> Type@{j})
   (t : G eq_refl) :
   simplified_ind_pack B x p G (simplify_ind_pack_inv B x p G t) = t.

theories/Type/Telescopes.v

@@ -141,7 +141,7 @@ Instance wf_tele_measure@{i j k| i <= k, j <= k}
          {T : tele@{i}} (A : Type@{j}) (f : tele_fn@{i j k} T A) (R : A -> A -> Type@{k}) :
   WellFounded R -> WellFounded (tele_measure T A f R) | (WellFounded (tele_measure _ _ _ _)).
 Proof.
-  intros. apply wf_inverse_image@{i j k k}. apply X.
+  intros. apply wf_inverse_image@{i j k}. apply X.
 Defined.
 
 Section Fix.