diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-24 18:05:27 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-24 18:05:27 +0000 |
| commit | 2337b9bfc662981a2630df8c173d54b32fa2b2b6 (patch) | |
| tree | c9499704a38542e1512f6955eaf8bcd24c2256e8 /tactics/tauto.ml4 | |
| parent | 44233ae7f65d3f1ff360667b867ef890e17e1e46 (diff) | |
A (safe) implementation of prolog's cut in the typeclasses eauto to avoid
redoing proofs for nothing, i.e, do not backtrack on proofs whose evars
are disjoint from the evars of the rest of the goals.
Fixes the example in bug #1911, needs some more testing.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11258 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tauto.ml4')
0 files changed, 0 insertions, 0 deletions