diff options
| author | aspiwack | 2013-11-02 15:34:26 +0000 |
|---|---|---|
| committer | aspiwack | 2013-11-02 15:34:26 +0000 |
| commit | 0a1202fae3a8ae8cf651c1b699545a8638ec579f (patch) | |
| tree | 652b6ae0fa3458d114467c31e1fe382bd1b755a3 /tactics/tactics.mllib | |
| parent | fe9258c4b228fb086baac7cd3d94207f2c43bb48 (diff) | |
A whole new implemenation of the refine tactic.
It now uses the same algorithm as pretyping does.
This produces pretty weird goal when refining pattern matching terms.
Modification of the pattern matching compilation algorithm are pending, hence I will let it be so for now.
The file Zsqrt_compat.v has two temporary [Admitted] related to this issue.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16973 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tactics.mllib')
| -rw-r--r-- | tactics/tactics.mllib | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index 0b97e08527..7b91665adf 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -13,7 +13,6 @@ Elim Auto Equality Contradiction -Refine Inv Leminv Tacsubst |