Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et commandes vernaculaires (cf dev/changements.txt pour plus de précisions)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2722 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 17 deletions

diff --git a/tactics/refine.ml b/tactics/refine.ml
index a942b37b7..d1f380e49 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -340,20 +340,3 @@ let refine oc gl =
   let th = compute_metamap env gmm c in
   tcc_aux th gl
 
-let refine_tac = Tacmach.hide_openconstr_tactic "Refine" refine
-
-open Proof_type
-
-let dyn_tcc args gl = match args with 
-  | [Command com]  ->
-      let env = pf_env gl in
-      refine
-	(Astterm.interp_casted_openconstr (project gl) env com (pf_concl gl))
-	gl
-  | [OpenConstr c] -> 
-      refine c gl
-  | _ -> assert false
-
-let tcc_tac = hide_tactic "Tcc" dyn_tcc
-
-