From b20e1be71f9b5c5585b214e30b5042676fa6cd46 Mon Sep 17 00:00:00 2001
From: delahaye
Date: Fri, 29 Dec 2000 19:23:25 +0000
Subject: Ajout du Let pour le langage de tactiques

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

(limited to 'tactics')

diff --git a/tactics/tacentries.ml b/tactics/tacentries.ml
index f7afda327b..852b0ff832 100644
--- a/tactics/tacentries.ml
+++ b/tactics/tacentries.ml
@@ -14,8 +14,6 @@ let v_transitivity  = hide_tactic "Transitivity"  dyn_transitivity
 let v_intro         = hide_tactic "Intro"         dyn_intro
 let v_intro_move    = hide_tactic "IntroMove"     dyn_intro_move
 let v_introsUntil   = hide_tactic "IntrosUntil"   dyn_intros_until
-(*i let v_tclIDTAC      = hide_tactic "Idtac"         dyn_tclIDTAC
-let v_tclFAIL       = hide_tactic "Fail"          dyn_tclFAIL i*)
 let v_assumption    = hide_tactic "Assumption"    dyn_assumption
 let v_exact         = hide_tactic "Exact"         dyn_exact_check
 let v_reduce        = hide_tactic "Reduce"        dyn_reduce
-- 
cgit v1.2.3