From 007234026bd8a435fa44ed672b223a3b3c6f83a6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 7 Apr 2003 09:37:35 +0000
Subject: code mort

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

diff --git a/tactics/elim.ml b/tactics/elim.ml
index 09c176ac68..85ff09f5c6 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -139,13 +139,6 @@ let h_decompose_or c =
 let h_decompose_and c =
   Refiner.abstract_tactic (TacDecomposeAnd c) (decompose_and c)
 
-(*
-let vernac_decompose_and = 
-  hide_constr_tactic "DecomposeAnd" decompose_and
-let vernac_decompose_or  = 
-  hide_constr_tactic  "DecomposeOr"  decompose_or
-*)
-
 (* The tactic Double performs a double induction *)
 
 let simple_elimination c gls =
-- 
cgit v1.2.3