From 60770e86f4ec925fce52ad3565a92beb98d253c1 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 15 Sep 2017 22:21:46 +0200 Subject: Stop exposing UState.universe_context and its Evd wrapper. We can enforce properties through check_univ_decl, or get an arbitrary ordered context with UState.context / Evd.to_universe_context (the later being a new wrapper of the former). --- tactics/leminv.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics/leminv.ml') diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 4d1b271d6..1ee873e0f 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -232,7 +232,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = let invProof = it_mkNamedLambda_or_LetIn c !ownSign in let invProof = EConstr.Unsafe.to_constr invProof in let p = Evarutil.nf_evars_universes sigma invProof in - p, Evd.universe_context ~names:[] ~extensible:true sigma + p, Evd.to_universe_context sigma let add_inversion_lemma name env sigma t sort dep inv_op = let invProof, univs = inversion_scheme env sigma t sort dep inv_op in -- cgit v1.2.3