diff options
| -rw-r--r-- | kernel/names.ml | 8 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 13 | ||||
| -rw-r--r-- | test-suite/success/Typeclasses.v | 8 |
3 files changed, 18 insertions, 11 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index 9267a64d61..1eb9a31751 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -34,9 +34,15 @@ struct let hash = String.hash + let warn_invalid_identifier = + CWarnings.create ~name:"invalid-identifier" ~category:"parsing" + ~default:CWarnings.Disabled + (fun s -> str s) + let check_soft ?(warn = true) x = let iter (fatal, x) = - if fatal then CErrors.error x else if warn then Feedback.msg_warning (str x) + if fatal then CErrors.error x else + if warn then warn_invalid_identifier x in Option.iter iter (Unicode.ident_refutation x) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index e44ace4257..b416bc657a 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1124,12 +1124,12 @@ module Search = struct else tclDISPATCH (List.init j (fun j' -> (tac_of gls i (Option.default 0 k + j)))) in - let finish sigma = + let finish nestedshelf sigma = let filter ev = try let evi = Evd.find_undefined sigma ev in if info.search_only_classes then - Some (ev, is_class_type sigma (Evd.evar_concl evi)) + Some (ev, not (is_class_type sigma (Evd.evar_concl evi))) else Some (ev, true) with Not_found -> None in @@ -1147,9 +1147,9 @@ module Search = struct begin (* Some existentials produced by the original tactic were not solved in the subgoals, turn them into subgoals now. *) - let shelved, goals = List.split_when (fun (ev, s) -> s) remaining in - let shelved = List.map fst shelved and goals = List.map fst goals in - if !typeclasses_debug > 1 && not (List.is_empty goals) then + let shelved, goals = List.partition (fun (ev, s) -> s) remaining in + let shelved = List.map fst shelved @ nestedshelf and goals = List.map fst goals in + if !typeclasses_debug > 1 && not (List.is_empty shelved && List.is_empty goals) then Feedback.msg_debug (str"Adding shelved subgoals to the search: " ++ prlist_with_sep spc (pr_ev sigma) goals ++ @@ -1162,7 +1162,8 @@ module Search = struct with_shelf (Unsafe.tclEVARS sigma' <*> Unsafe.tclNEWGOALS goals) >>= fun s -> result s i (Some (Option.default 0 k + j))) end - in res <*> tclEVARMAP >>= finish + in with_shelf res >>= fun (sh, ()) -> + tclEVARMAP >>= finish sh in if path_matches derivs [] then aux e tl else diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index f62427ef47..6b1f0315bc 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -98,7 +98,7 @@ Goal exists R, @Refl nat R. solve [typeclasses eauto with foo]. Qed. -(* Set Typeclasses Compatibility "8.5". *) +Set Typeclasses Compatibility "8.5". Parameter f : nat -> Prop. Parameter g : nat -> nat -> Prop. Parameter h : nat -> nat -> nat -> Prop. @@ -108,8 +108,7 @@ Axiom c : forall x y z, h x y z -> f x -> f y. Hint Resolve a b c : mybase. Goal forall x y z, h x y z -> f x -> f y. intros. - Set Typeclasses Debug. - typeclasses eauto with mybase. + Fail Timeout 1 typeclasses eauto with mybase. (* Loops now *) Unshelve. Abort. End bt. @@ -138,7 +137,8 @@ Notation "'return' t" := (unit t). Class A `(e: T) := { a := True }. Class B `(e_: T) := { e := e_; sg_ass :> A e }. -Set Typeclasses Debug. +(* Set Typeclasses Debug. *) +(* Set Typeclasses Debug Verbosity 2. *) Goal forall `{B T}, Prop. intros. apply a. |