diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2016-11-30 15:00:13 +0100 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2016-11-30 16:41:47 +0100 |
| commit | 823f0ab9c34f99d9171a5332a535c20d9f0f315c (patch) | |
| tree | 53821ba9a73ebe229b1408472504e8a147d2497d /tactics/class_tactics.ml | |
| 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.
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index e44ace425..b47d8af56 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 |