diff options
| -rw-r--r-- | doc/refman/Classes.tex | 13 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 24 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3513.v | 3 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4095.v | 4 | ||||
| -rw-r--r-- | test-suite/success/Typeclasses.v | 2 | ||||
| -rw-r--r-- | test-suite/success/bteauto.v | 6 |
6 files changed, 15 insertions, 37 deletions
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index 58ae7191f..7c4bd4d20 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -392,13 +392,12 @@ than {\tt eauto} and {\tt auto}. The main differences are the following: backtracking on subgoals that are entirely independent. \item When called with no arguments, {\tt typeclasses eauto} uses the {\tt typeclass\_instances} database by default (instead of {\tt core}) - and will try to solve \emph{only} typeclass goals. If some subgoal of - a hint/instance is non-dependent and not of class type, that hint - application will fail. Dependent subgoals are automatically shelved - and \emph{must be} resolved entirely when the other typeclass subgoals - are resolved or the proof search will fail \emph{globally}, - \emph{without} the possibility to find another complete solution with - no shelved subgoals. + and will try to solve \emph{only} typeclass goals, shelving the other + goals. If some subgoal of a hint/instance is non-dependent and not of + class type, the hint application will fail when faced with that + subgoal. Dependent subgoals are automatically shelved, and shelved + goals can remain after resolution ends (following the behavior of + \Coq{} 8.5). \emph{Note: } As of Coq 8.6, {\tt all:once (typeclasses eauto)} faithfully mimicks what happens during typeclass resolution when it is diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 262b30893..99a1a9899 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 = diff --git a/test-suite/bugs/closed/3513.v b/test-suite/bugs/closed/3513.v index ff515038e..9ed0926a6 100644 --- a/test-suite/bugs/closed/3513.v +++ b/test-suite/bugs/closed/3513.v @@ -89,5 +89,6 @@ Debug: 2.2.1.1.1.1: apply ILFun_ILogic on (ILogic OPred) Show Existentials. Set Typeclasses Debug Verbosity 2. Set Printing All. - Fail apply reflexivity. + (* As in 8.5, allow a shelved subgoal to remain *) + apply reflexivity.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4095.v b/test-suite/bugs/closed/4095.v index 83d4ed69d..ffd33d381 100644 --- a/test-suite/bugs/closed/4095.v +++ b/test-suite/bugs/closed/4095.v @@ -1,10 +1,10 @@ (* File reduced by coq-bug-finder from original input, then from 5752 lines to 3828 lines, then from 2707 lines to 558 lines, then from 472 lines to 168 lines, then from 110 lines to 101 lines, then from 96 lines to 77 lines, then from 80 lines to 64 lines, then from 92 lines to 79 lines *) (* coqc version 8.5beta1 (February 2015) compiled on Feb 23 2015 18:32:3 with OCaml 4.01.0 coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (ebfc19d792492417b129063fb511aa423e9d9e08) *) -Require Import TestSuite.admit. Require Import Coq.Setoids.Setoid. Generalizable All Variables. Axiom admit : forall {T}, T. +Ltac admit := apply admit. Class Equiv (A : Type) := equiv : relation A. Class type (A : Type) {e : Equiv A} := eq_equiv : Equivalence equiv. Class ILogicOps Frm := { lentails: relation Frm; @@ -71,7 +71,7 @@ Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred) refine (P _ _) end. Undo. - lazymatch goal with + Fail lazymatch goal with | |- ?R (?f ?a ?b) (?f ?a' ?b') => let P := constr:(fun H H' => Morphisms.proper_prf a a' H b b' H') in set(p:=P) diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index 6885717ec..5557ba837 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -6,7 +6,7 @@ Module onlyclasses. Goal Foo * Foo. split. shelve. Set Typeclasses Debug. - Fail typeclasses eauto. + Fail (unshelve typeclasses eauto); fail. typeclasses eauto with typeclass_instances. Unshelve. typeclasses eauto with typeclass_instances. Qed. diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v index 3178c6fc1..0af367781 100644 --- a/test-suite/success/bteauto.v +++ b/test-suite/success/bteauto.v @@ -24,9 +24,9 @@ Module Backtracking. Fail all:((once (typeclasses eauto with typeclass_instances)) + apply eq_refl). (* Does backtrack if other goals fail *) - all:[> typeclasses eauto + reflexivity .. ]. + all:[> (unshelve typeclasses eauto; fail) + reflexivity .. ]. Undo 1. - all:(typeclasses eauto + reflexivity). (* Note "+" is a focussing combinator *) + all:((unshelve typeclasses eauto; fail) + reflexivity). (* Note "+" is a focussing combinator *) Show Proof. Qed. @@ -66,7 +66,7 @@ Module Backtracking. unshelve evar (t : A). all:cycle 1. refine (@ex_intro _ _ t _). all:cycle 1. - all:(typeclasses eauto + reflexivity). + all:((unshelve typeclasses eauto; fail) + reflexivity). Qed. End Leivant. End Backtracking. |