diff options
author | 2016-10-26 18:33:08 +0200 | |
---|---|---|
committer | 2016-11-03 16:26:39 +0100 | |
commit | 8aa945902d40765f69cd16ce7647d3c28248eb54 (patch) | |
tree | 812b336499f03ebde55419019b91e779fea3d29d /tactics/class_tactics.ml | |
parent | 59b4938c3a763e0ed35dd8f91f5d45b286df01a6 (diff) |
Handle Unique Solutions flag.
Diffstat (limited to 'tactics/class_tactics.ml')
-rw-r--r-- | tactics/class_tactics.ml | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 8ec005a60..c1a2f7ff2 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -9,7 +9,6 @@ (* TODO: - Find an interface allowing eauto to backtrack when shelved goals remain, e.g. to force instantiations. - - unique solutions *) open Pp @@ -1256,6 +1255,9 @@ module Search = struct Tacticals.New.tclFAIL 0 (str"Proof search failed" ++ (if Option.is_empty depth then mt() else str" without reaching its limit")) + | Proofview.MoreThanOneSuccess -> + Tacticals.New.tclFAIL 0 (str"Proof search failed: " ++ + str"more than one success found.") | e -> Proofview.tclZERO ~info:ie e in Proofview.tclOR tac error @@ -1273,6 +1275,11 @@ module Search = struct let _, pv = Proofview.init evm' [] in let pv = Proofview.unshelve goals pv in try + let tac = + if unique then + Proofview.tclEXACTLY_ONCE Proofview.MoreThanOneSuccess tac + else tac + in let (), pv', (unsafe, shelved, gaveup), _ = Proofview.apply (Global.env ()) tac pv in @@ -1292,7 +1299,7 @@ module Search = struct with Logic_monad.TacticFailure _ -> raise Not_found let eauto depth only_classes unique dep st hints p evd = - let eauto_tac = eauto_tac ~st ~only_classes ~depth ~dep hints in + let eauto_tac = eauto_tac ~st ~only_classes ~depth ~dep:(unique || dep) hints in let res = run_on_evars ~unique p evd eauto_tac in match res with | None -> evd |