From cb738f93e74b2d11bc5a67e75cf5f6f07e676d77 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 18 Jan 2009 17:58:23 +0000
Subject: Getting rid of the previous implementation of setoid_rewrite which
 was unplugged a long time ago.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11798 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/extraargs.ml4 | 16 ----------------
 1 file changed, 16 deletions(-)

(limited to 'tactics/extraargs.ml4')

diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index f02ef6dfc4..0eb4a76f3a 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -98,22 +98,6 @@ ARGUMENT EXTEND occurrences
 | [ var(id) ] -> [ ArgVar id ]
 END
 
-(* For Setoid rewrite *)
-let pr_morphism_signature _ _ _ s =
-  spc () ++ Setoid_replace.pr_morphism_signature s
-
-ARGUMENT EXTEND morphism_signature
- TYPED AS morphism_signature
- PRINTED BY pr_morphism_signature
-  | [ constr(out) ] -> [ [],out ]
-  | [ constr(c) "++>" morphism_signature(s) ] ->
-       [ let l,out = s in (Some true,c)::l,out ]
-  | [ constr(c) "-->" morphism_signature(s) ] ->
-       [ let l,out = s in (Some false,c)::l,out ]
-  | [ constr(c) "==>" morphism_signature(s) ] ->
-       [ let l,out = s in (None,c)::l,out ]
-END
-
 let pr_gen prc _prlc _prtac c = prc c
 
 let pr_rawc _prc _prlc _prtac raw = Printer.pr_rawconstr raw
-- 
cgit v1.2.3