diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-03-24 16:15:32 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-03-24 16:15:32 +0100 |
| commit | af291869bb7d1184d8e655906572d75937ca829b (patch) | |
| tree | 62a5ccf9ee7b115b7d1118cbc3db92c553261713 /tactics/class_tactics.ml | |
| parent | 3234a893a1b3cfd6b51f1c26cc10e9690d8a703e (diff) | |
| parent | 7535e268f7706d1dee263fdbafadf920349103db (diff) | |
Merge branch 'trunk' into pr379
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 64d76360f..c53e47d92 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1614,11 +1614,15 @@ let is_ground c gl = if Evarutil.is_ground_term (project gl) c then tclIDTAC gl else tclFAIL 0 (str"Not ground") gl -let autoapply c i = Proofview.Goal.enter { enter = begin fun gl -> +let autoapply c i = + let open Proofview.Notations in + Proofview.Goal.enter { enter = begin fun gl -> let flags = auto_unif_flags Evar.Set.empty (Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in let cty = Tacmach.New.pf_unsafe_type_of gl c in let ce = mk_clenv_from gl (c,cty) in - (unify_e_resolve false flags).enter gl - ((c,cty,Univ.ContextSet.empty),0,ce) -end } + (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) end } |