diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-03-10 09:24:29 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-03-10 09:24:29 +0100 |
| commit | 74285d3fe7e65848e30caf147f9032c68547822b (patch) | |
| tree | 0fed7232d2f60ca3d5a8e42386d3f69c2f149d9b /tactics/class_tactics.ml | |
| parent | d30d5a9b32e020586d265f8e879c287269c17575 (diff) | |
| parent | c694b91bba898aad1e071d91fa70b7c5574cbf98 (diff) | |
Merge PR#359: Fix bug 4969, autoapply was not tagging shelved subgoals correctly as…
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index b416bc657..d1ae85e7b 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1604,10 +1604,16 @@ let is_ground c gl = else tclFAIL 0 (str"Not ground") gl let autoapply c i gl = + let open Proofview.Notations in let flags = auto_unif_flags Evar.Set.empty (Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in let cty = pf_unsafe_type_of gl c in let ce = mk_clenv_from gl (c,cty) in - let tac = { enter = fun gl -> (unify_e_resolve false flags).enter gl - ((c,cty,Univ.ContextSet.empty),0,ce) } in - Proofview.V82.of_tactic (Proofview.Goal.nf_enter tac) gl + let enter gl = + (unify_e_resolve false flags).enter gl + ((c,cty,Univ.ContextSet.empty),0,ce) <*> + Proofview.tclEVARMAP >>= (fun sigma -> + let sigma = Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals sigma in + Proofview.Unsafe.tclEVARS sigma) + in + Proofview.V82.of_tactic (Proofview.Goal.nf_enter { enter }) gl |