diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-02 14:58:00 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-06 13:41:24 +0100 |
| commit | 5d926b0279f70250db1ee54edcdb4e855ac96f0f (patch) | |
| tree | 06dc436ba2d41764b5bbe48c311bdaeaf5c1514c /vernac/auto_ind_decl.ml | |
| parent | 67a28c487fc64e2c0f8271b77d0c9db0cd82fa92 (diff) | |
Deprecate UState aliases in Evd.
Diffstat (limited to 'vernac/auto_ind_decl.ml')
| -rw-r--r-- | vernac/auto_ind_decl.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 9b7b88b51..2879feba7 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -323,7 +323,7 @@ let build_beq_scheme mode kn = raise NoDecidabilityCoInductive; let fix = mkFix (((Array.make nb_ind 0),i),(names,types,cores)) in create_input fix), - Evd.make_evar_universe_context (Global.env ()) None), + UState.make (Global.universes ())), !eff let beq_scheme_kind = declare_mutual_scheme_object "_beq" build_beq_scheme @@ -671,7 +671,7 @@ let make_bl_scheme mode mind = let lnonparrec,lnamesparrec = (* TODO subst *) context_chop (nparams-nparrec) mib.mind_params_ctxt in let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in - let ctx = Evd.make_evar_universe_context (Global.env ()) None in + let ctx = UState.make (Global.universes ()) in let side_eff = side_effect_of_mode mode in let bl_goal = EConstr.of_constr bl_goal in let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx bl_goal @@ -795,7 +795,7 @@ let make_lb_scheme mode mind = let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in - let ctx = Evd.make_evar_universe_context (Global.env ()) None in + let ctx = UState.make (Global.universes ()) in let side_eff = side_effect_of_mode mode in let lb_goal = EConstr.of_constr lb_goal in let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx lb_goal @@ -965,7 +965,7 @@ let make_eq_decidability mode mind = let nparams = mib.mind_nparams in let nparrec = mib.mind_nparams_rec in let u = Univ.Instance.empty in - let ctx = Evd.make_evar_universe_context (Global.env ()) None in + let ctx = UState.make (Global.universes ()) in let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in let side_eff = side_effect_of_mode mode in |