diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-12-16 10:19:06 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-12-16 10:19:06 +0000 |
| commit | 6fabdb398ffedd3f3ffdef3cd02b8749be20445b (patch) | |
| tree | fbf1765941a0f4f620b81c9ffc59006acd02e91a /tactics/extratactics.ml4 | |
| parent | 302571c0740f4a93ef1350901e2ab1add792597b (diff) | |
Finish fix for the treatment of [inverse] in [setoid_rewrite], making a
variant of the [unify] tactic that takes a hint db as argument and does
unification modulo its [transparent_state]. Add test-file for bug #1939
and another [AdvancedTypeClasses.v] that mimicks
[AdvancedCanonicalStructure.v].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11685 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/extratactics.ml4')
| -rw-r--r-- | tactics/extratactics.ml4 | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 62ac0d4d7..285aec91c 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -499,10 +499,6 @@ TACTIC EXTEND dependent_pattern | ["dependent_pattern" constr(c) ] -> [ dependent_pattern c ] END -TACTIC EXTEND conv -| ["conv" constr(x) constr(y) ] -> [ conv x y ] -END - TACTIC EXTEND resolve_classes | ["resolve_classes" ] -> [ resolve_classes ] END |