diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-12-18 12:19:12 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-12-18 12:19:12 +0000 |
| commit | f3eaf2869e84c942d56a7fe0cc459d9943e4b059 (patch) | |
| tree | 4a67e700f35e74324cece25f50325758e43dcb03 /tactics | |
| parent | 0e1b31da1546b7ac0dd3664e73ba05127320bed9 (diff) | |
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
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/extratactics.ml4 | 17 |
1 files changed, 0 insertions, 17 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index ef6ac60f4..0fff16cf9 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 |