Add env universes to eqschemes ucontexts

Author: yannl35133

engine/uState.ml

@@ -488,7 +488,10 @@ let univ_entry ~poly uctx =
 
 let of_context_set ((qs,us),csts) =
   let sort_variables = QState.of_set qs in
+  let univs = Level.Set.fold (UGraph.add_universe ~strict:false) us UGraph.initial_universes in
   { empty with
+    initial_universes = univs;
+    universes = univs;
     local = (us,csts);
     sort_variables;}
 

tactics/eqschemes.ml

@@ -76,6 +76,9 @@ let fresh env id avoid =
 let with_context_set ctx (b, ctx') =
   (b, UnivGen.sort_context_union ctx ctx')
 
+let of_context_set env ctx =
+  UState.merge_sort_context ~sideff:false UnivRigid QGraph.Internal (UState.from_env env) ctx
+
 let build_dependent_inductive ind (mib,mip) =
   let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in
   applist
@@ -230,7 +233,7 @@ let build_sym_scheme env _handle ind =
             mkRel 1 (* varH *),
             [|cstr (nrealargs+1)|])))))
   in
-  c, UState.of_context_set ctx
+  c, of_context_set env ctx
 
 let sym_scheme_kind =
   declare_individual_scheme_object "sym"
@@ -301,7 +304,7 @@ let build_sym_involutive_scheme env handle ind =
                NoInvert,
                mkRel 1 (* varH *),
                [|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|])))))
-  in (c, UState.of_context_set ctx)
+  in (c, of_context_set env ctx)
 
 let sym_involutive_scheme_kind =
   declare_individual_scheme_object "sym_involutive"
@@ -461,7 +464,7 @@ let build_l2r_rew_scheme dep env handle ind kind =
        [|main_body|]))
    else
      main_body))))))
-  in (c, UState.of_context_set ctx)
+  in (c, of_context_set env ctx)
 
 (**********************************************************************)
 (* Build the left-to-right rewriting lemma for hypotheses associated  *)
@@ -554,7 +557,7 @@ let build_l2r_forward_rew_scheme dep env ind kind =
           (if dep then realsign_ind_P 1 applied_ind_P' else realsign_P 2) s)
       (mkNamedLambda (make_annot varHC sr) applied_PC'
         (mkVar varHC))|]))))))
-  in c, UState.of_context_set ctx
+  in c, of_context_set env ctx
 
 (**********************************************************************)
 (* Build the right-to-left rewriting lemma for hypotheses associated  *)
@@ -641,7 +644,7 @@ let build_r2l_forward_rew_scheme dep env ind kind =
            lift (nrealargs+3) applied_PC,
            mkRel 1)|])),
     [|mkVar varHC|]))))))
-  in c, UState.of_context_set ctx
+  in c, of_context_set env ctx
 
 (**********************************************************************)
 (* This function "repairs" the non-dependent r2l forward rewriting    *)
@@ -859,7 +862,7 @@ let build_congr env (eq,refl,ctx) ind =
        [|mkApp (refl,
           [|mkVar varB;
             mkApp (mkVar varf, [|lift (mip.mind_nrealargs+3) b|])|])|])))))))
-  in c, UState.of_context_set ctx
+  in c, of_context_set env ctx
 
 let congr_scheme_kind = declare_individual_scheme_object "congr"
   (fun env _ ind ->

vernac/indschemes.ml

@@ -380,7 +380,7 @@ let do_mutual_induction_scheme ~register ?(force_mutual=false) env ?(isrec=true)
     let _, ctx = Typeops.type_of_global_in_context env (Names.GlobRef.IndRef ind) in
     let u, ctx = UnivGen.fresh_instance_from ctx None in
     let u = EConstr.EInstance.make u in
-    let sigma = Evd.from_ctx (UState.of_context_set ctx) in
+    let sigma = Evd.from_ctx (UState.(union (from_env env) (of_context_set ctx))) in
     sigma, u
   in
   let sigma, lrecspec =