From f3eaf2869e84c942d56a7fe0cc459d9943e4b059 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Tue, 18 Dec 2007 12:19:12 +0000
Subject: Nettoyage de code en vue de la release. Plus de Warning: Unused
 Variable, et plus de trucs useless qui traînaient par ma faute (y compris
 dans le noyau, la honte).

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

(limited to 'tactics')

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index ef6ac60f44..0fff16cf92 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -413,23 +413,6 @@ VERNAC COMMAND EXTEND RetroknowledgeRegister
              Global.register f tc tb ]
 END
 
-(* spiwack : Vernac commands for developement *)
-
-(* arnaud : comment out/clear ? *)
-VERNAC COMMAND EXTEND InternalRepresentation (* Prints internal representation of the argument *)
-| [ "Internal" "Representation" "of" constr(t) ] -> 
-    [ let t' = Constrintern.interp_constr Evd.empty (Global.env ()) t in
-      pp (str (string_of_constr t'))]
-END
-
-VERNAC COMMAND EXTEND Bytecode (* Prints Bytecode representation of the argument *)
-| [ "Bytecode" "of" constr(t) ] -> 
-    [ let t' = Constrintern.interp_constr Evd.empty (Global.env ()) t in
-      let (bc,_,_) = Cbytegen.compile (Environ.pre_env (Global.env ())) t' in
-      pp (str (Cbytecodes.string_of_instr bc))]
-END
-
-(* /spiwack *)
 
 
 TACTIC EXTEND apply_in
-- 
cgit v1.2.3