diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-06-24 17:10:49 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-06-27 23:13:52 +0200 |
| commit | 6ae5029770567b11f5872d33be63357ff3a0cb17 (patch) | |
| tree | 6c31e5522a9056043a018d88bca78a0dc4c39261 /tactics/class_tactics.ml | |
| parent | c9451add699a3e567eefa9de96426b86a4648edd (diff) | |
Typeclasses: mark unresolvable goals in new implementation
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 16 |
1 files changed, 14 insertions, 2 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 3fca7f50d..211e46c07 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -982,6 +982,14 @@ module Search = struct occur_existential concl else true + let mark_unresolvables sigma goals = + List.fold_left + (fun sigma gl -> + let evi = Evd.find_undefined sigma gl in + let evi' = Typeclasses.mark_unresolvable evi in + Evd.add sigma gl evi') + sigma goals + (** The general hint application tactic. tac1 + tac2 .... The choice of OR or ORELSE is determined depending on the dependencies of the goal and the unique/Prop @@ -1089,10 +1097,14 @@ module Search = struct if !typeclasses_debug > 1 then Feedback.msg_debug (str"Adding shelved subgoals to the search: " ++ - prlist_with_sep spc (pr_ev sigma) goals); + prlist_with_sep spc (pr_ev sigma) goals ++ + str" while shelving " ++ + prlist_with_sep spc (pr_ev sigma) shelved); shelve_goals shelved <*> (if List.is_empty goals then tclUNIT () - else with_shelf (Unsafe.tclNEWGOALS goals) >>= + else + let sigma' = mark_unresolvables sigma goals in + with_shelf (Unsafe.tclEVARS sigma' <*> Unsafe.tclNEWGOALS goals) >>= fun s -> result s i (Some (Option.default 0 k + j))) end in res <*> tclEVARMAP >>= finish |