diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-04 13:04:18 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-04 13:21:58 +0200 |
| commit | aab836160c3a963dc324f323cb62086d19127320 (patch) | |
| tree | 71796849dfa35d79d0b0317c8ec958e870e85db1 /tactics/tactics.ml | |
| parent | 075c099b1777eea32c3a392cc039723c15c5b66e (diff) | |
Adding a tclUPDATE_ENV primitive and using it in in tclABSTRACT.
Hopefully, this may fix some nasty bugs lying around.
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0c69f5088..77876e626 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3939,8 +3939,13 @@ let abstract_subproof id gk tac = let effs = cons_side_effects eff Entries.(snd (Future.force const.const_entry_body)) in let args = List.rev (instance_from_named_context sign) in - let solve = Proofview.V82.tclEVARS evd <*> - Proofview.tclEFFECTS effs <*> new_exact_no_check (applist (lem, args)) in + let solve = + Proofview.V82.tclEVARS evd <*> + Proofview.tclEFFECTS effs <*> + (** Hack around *) + Proofview.tclUPDATE_ENV (Global.env ()) <*> + new_exact_no_check (applist (lem, args)) + in if not safe then Proofview.mark_as_unsafe <*> solve else solve end |