Commit 93ad2443 authored by Michael Sammler's avatar Michael Sammler
Browse files

ensure that there is no bad backtracking

parent 567f11f2
Pipeline #52430 passed with stage
in 33 minutes and 11 seconds
......@@ -528,8 +528,8 @@ Ltac liFindInContext :=
multiple implementations of [FindInContext]. They are tried in the
order of their priorities.
See https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Multi-success.20TC.20resolution.20from.20ltac.3F/near/242759123 *)
simple notypeclasses refine (tac_fast_apply ((_ : FindInContext fic key) _).(i2p_proof) _);
[ shelve | typeclasses eauto | simpl; repeat liExist false; liFindHypOrTrue key ]
once (simple notypeclasses refine (tac_fast_apply ((_ : FindInContext fic key) _).(i2p_proof) _);
[ shelve | typeclasses eauto | simpl; repeat liExist false; liFindHypOrTrue key ])
end.
Ltac liTrue :=
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment