diff options
| author | Matthieu Sozeau | 2016-11-15 13:53:57 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-11-15 14:54:05 +0100 |
| commit | 4b8f19c58a2b6cc841db2c011d23aa8106211fd6 (patch) | |
| tree | ade3adfabf9e288a164769e0457fda6e49ac1b24 /tactics | |
| parent | dfefd12ee432e5b0d145934e74bb939ddecfa522 (diff) | |
Revert part of a477dc, disallow_shelved
In only_classes mode we do not try to implement a stricter semantics for
shelved goals in 8.6. Leaving this for 8.7.
Update the documentation as well.
Remove a spurious printf call as well.
Fix test-suite now that shelved goals are allowed
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 24 |
1 files changed, 1 insertions, 23 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 262b308932..99a1a98993 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1176,7 +1176,7 @@ module Search = struct (fun e' -> if CErrors.noncritical (fst e') then (pr_error e'; aux (merge_exceptions e e') tl) - else (Printf.printf "raising again\n%!"; iraise e')) + else iraise e') and aux e = function | x :: xs -> onetac e x xs | [] -> @@ -1274,27 +1274,6 @@ module Search = struct | (e,ie) -> Proofview.tclZERO ~info:ie e) in aux 1 - let disallow_shelved initshelf tac = - let open Proofview in - let casefn = function - | Fail (e,info) -> tclZERO ~info e - | Next ((shelved, result), k) -> - if not (List.is_empty shelved) then - begin - Proofview.tclEVARMAP >>= fun sigma -> - let gls = prlist_with_sep spc (pr_ev sigma) shelved in - (if !typeclasses_debug > 0 then - let initgls = prlist_with_sep spc (pr_ev sigma) initshelf in - Feedback.msg_debug (str"Non-empty shelf at end of resolution:" ++ gls - ++ str" initially: " ++ initgls ++ str".")); - Tacticals.New.tclZEROMSG (str"Proof search failed: " ++ - str"shelved goals remain: " ++ gls) - end - else - tclOR (tclUNIT result) (fun e -> k e >>= fun (gls, result) -> tclUNIT result) - in - tclCASE (with_shelf tac) >>= casefn - let eauto_tac ?(st=full_transparent_state) ?(unique=false) ~only_classes ?strategy ~depth ~dep hints = let open Proofview in @@ -1342,7 +1321,6 @@ module Search = struct str " in regular mode" ++ match depth with None -> str ", unbounded" | Some i -> str ", with depth limit " ++ int i)); - let tac = if only_classes then disallow_shelved initshelf tac else tac in tac let run_on_evars p evm tac = |