diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2013-12-13 16:39:44 +0000 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:58:57 +0200 |
| commit | 29794b8acf407518716f8c02c2ed20729f8802e5 (patch) | |
| tree | a7952e066c733ed10af5a5f43fcbff3ab960971d /tactics | |
| parent | 55e62174683f293c8f966d8bd486fcb511f66221 (diff) | |
- Fix abstract forgetting about new constraints.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 |