diff options
| author | Gaëtan Gilbert | 2018-03-02 14:58:00 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-03-06 13:41:24 +0100 |
| commit | 5d926b0279f70250db1ee54edcdb4e855ac96f0f (patch) | |
| tree | 06dc436ba2d41764b5bbe48c311bdaeaf5c1514c /tactics | |
| parent | 67a28c487fc64e2c0f8271b77d0c9db0cd82fa92 (diff) | |
Deprecate UState aliases in Evd.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/eqschemes.ml | 12 | ||||
| -rw-r--r-- | tactics/ind_tables.ml | 4 |
2 files changed, 8 insertions, 8 deletions
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 45926551b4..477de6452e 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -214,7 +214,7 @@ let build_sym_scheme env ind = rel_vect (2*nrealargs+2) nrealargs])), mkRel 1 (* varH *), [|cstr (nrealargs+1)|])))) - in c, Evd.evar_universe_context_of ctx + in c, UState.of_context_set ctx let sym_scheme_kind = declare_individual_scheme_object "_sym_internal" @@ -285,7 +285,7 @@ let build_sym_involutive_scheme env ind = mkRel 1|])), mkRel 1 (* varH *), [|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|])))) - in (c, Evd.evar_universe_context_of ctx), eff + in (c, UState.of_context_set ctx), eff let sym_involutive_scheme_kind = declare_individual_scheme_object "_sym_involutive" @@ -439,7 +439,7 @@ let build_l2r_rew_scheme dep env ind kind = [|main_body|]) else main_body)))))) - in (c, Evd.evar_universe_context_of ctx), + in (c, UState.of_context_set ctx), Safe_typing.concat_private eff' eff (**********************************************************************) @@ -528,7 +528,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 varHC applied_PC' (mkVar varHC))|]))))) - in c, Evd.evar_universe_context_of ctx + in c, UState.of_context_set ctx (**********************************************************************) (* Build the right-to-left rewriting lemma for hypotheses associated *) @@ -601,7 +601,7 @@ let build_r2l_forward_rew_scheme dep env ind kind = lift (nrealargs+3) applied_PC, mkRel 1)|]), [|mkVar varHC|])))))) - in c, Evd.evar_universe_context_of ctx + in c, UState.of_context_set ctx (**********************************************************************) (* This function "repairs" the non-dependent r2l forward rewriting *) @@ -808,7 +808,7 @@ let build_congr env (eq,refl,ctx) ind = [|mkApp (refl, [|mkVar varB; mkApp (mkVar varf, [|lift (mip.mind_nrealargs+3) b|])|])|])))))) - in c, Evd.evar_universe_context_of ctx + in c, UState.of_context_set ctx let congr_scheme_kind = declare_individual_scheme_object "_congr" (fun _ ind -> diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index b960a845ce..71e2d58201 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -122,8 +122,8 @@ let compute_name internal id = let define internal id c p univs = let fd = declare_constant ~internal in let id = compute_name internal id in - let ctx = Evd.normalize_evar_universe_context univs in - let c = Universes.subst_opt_univs_constr (Evd.evar_universe_context_subst ctx) c in + let ctx = UState.normalize univs in + let c = Universes.subst_opt_univs_constr (UState.subst ctx) c in let univs = if p then Polymorphic_const_entry (UState.context ctx) else Monomorphic_const_entry (UState.context_set ctx) |