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
---
 toplevel/vernacentries.ml | 1 -
 toplevel/vernacexpr.ml    | 1 -
 2 files changed, 2 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 37e9cf22ae..ab3df8c0c3 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1092,7 +1092,6 @@ let vernac_print = function
   | PrintHintDbName s -> Auto.print_hint_db_by_name s
   | PrintRewriteHintDbName s -> Autorewrite.print_rewrite_hintdb s
   | PrintHintDb -> Auto.print_searchtable ()
-  | PrintSetoids -> Setoid_replace.print_setoids()
   | PrintScopes ->
       pp (Notation.pr_scopes (Constrextern.without_symbols pr_lrawconstr))
   | PrintScope s ->
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 9412a5981c..aa6a48d66e 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -60,7 +60,6 @@ type printable =
   | PrintHintDbName of string
   | PrintRewriteHintDbName of string
   | PrintHintDb
-  | PrintSetoids
   | PrintScopes
   | PrintScope of string
   | PrintVisibility of string option
-- 
cgit v1.2.3