From a59bdc4144476c0794ff24fc6180e21671842395 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 12 Jul 2017 17:57:22 +0200 Subject: Removing the uses of abstraction-breaking code in Lemmas. I had to slightly tweak a test in order to work around a bug of simpl that loses universes constraints when refolding polymorphic fixpoints. --- vernac/lemmas.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'vernac') diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index cfd489dde..645320c60 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -44,12 +44,14 @@ let call_hook fix_exn hook l c = (* Support for mutually proved theorems *) -let retrieve_first_recthm = function +let retrieve_first_recthm uctx = function | VarRef id -> (NamedDecl.get_value (Global.lookup_named id),variable_opacity id) | ConstRef cst -> let cb = Global.lookup_constant cst in - let map (c, ctx) = Vars.subst_instance_constr (Univ.AUContext.instance ctx) c in + let (_, uctx) = UState.universe_context uctx in + let inst = Univ.UContext.instance uctx in + let map (c, ctx) = Vars.subst_instance_constr inst c in (Option.map map (Global.body_of_constant_body cb), is_opaque cb) | _ -> assert false @@ -413,7 +415,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook = let other_thms_data = if List.is_empty other_thms then [] else (* there are several theorems defined mutually *) - let body,opaq = retrieve_first_recthm ref in + let body,opaq = retrieve_first_recthm ctx ref in let subst = Evd.evar_universe_context_subst ctx in let norm c = Universes.subst_opt_univs_constr subst c in let ctx = UState.context_set (*FIXME*) ctx in -- cgit v1.2.3