diff options
| author | Théo Zimmermann | 2016-11-30 15:00:13 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2016-11-30 16:41:47 +0100 |
| commit | 823f0ab9c34f99d9171a5332a535c20d9f0f315c (patch) | |
| tree | 53821ba9a73ebe229b1408472504e8a147d2497d | |
| parent | 3e6fa1cbdc0ec145728089000595b6ea29f37a4c (diff) | |
Fix typeclasses eauto shelving.
A file in the test-suite had to be modified.
It was supposed to reproduce a behavior in intuistionistic-nuprl
but it did not really.
This commit is not supposed to break intuistionistic-nuprl.
| -rw-r--r-- | tactics/class_tactics.ml | 4 | ||||
| -rw-r--r-- | test-suite/success/Typeclasses.v | 8 |
2 files changed, 6 insertions, 6 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index e44ace4257..b47d8af56b 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1129,7 +1129,7 @@ module Search = struct 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,7 +1147,7 @@ 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, goals = List.partition (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 Feedback.msg_debug 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. |