From 6fabdb398ffedd3f3ffdef3cd02b8749be20445b Mon Sep 17 00:00:00 2001 From: msozeau Date: Tue, 16 Dec 2008 10:19:06 +0000 Subject: 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 --- tactics/extratactics.ml4 | 4 ---- 1 file changed, 4 deletions(-) (limited to 'tactics/extratactics.ml4') 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 -- cgit v1.2.3