From 29794b8acf407518716f8c02c2ed20729f8802e5 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 13 Dec 2013 16:39:44 +0000 Subject: - Fix abstract forgetting about new constraints. --- tactics/tactics.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 764f06a0f..cc1096e7c 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3763,8 +3763,8 @@ let abstract_subproof id tac = (** ppedrot: seems legit to have abstracted subproofs as local*) let cst = Declare.declare_constant ~internal:Declare.KernelSilent ~local:true id decl in (* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *) - (* FIXME: lem might have generated new constraints... not taken into account *) - let lem = Universes.unsafe_constr_of_global (ConstRef cst) in + let lem, ctx = Universes.unsafe_constr_of_global (ConstRef cst) in + let evd = Evd.merge_context_set Evd.univ_flexible evd (Univ.ContextSet.of_context ctx) in let open Declareops in let eff = Safe_typing.sideff_of_con (Global.safe_env ()) cst in let effs = cons_side_effects eff no_seff in -- cgit v1.2.3