mise a jour du nouveau ring et ajout du nouveau field, avant renommages

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

2 files changed, 5 insertions, 44 deletions

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 48c9238e05..9d5fb31511 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -157,31 +157,6 @@ let leaf g =
     goal = g;
     ref = None }
 
-(* Tactics table. *)
-
-let tac_tab = Hashtbl.create 17
-
-let add_tactic s t =
-  if Hashtbl.mem tac_tab s then
-    errorlabstrm ("Refiner.add_tactic: ") 
-      (str ("Cannot redeclare tactic "^s));
-  Hashtbl.add tac_tab s t
-
-let overwriting_add_tactic s t =
-  if Hashtbl.mem tac_tab s then begin
-    Hashtbl.remove tac_tab s;
-    warning ("Overwriting definition of tactic "^s)
-  end;
-  Hashtbl.add tac_tab s t
-
-let lookup_tactic s =
-  try 
-    Hashtbl.find tac_tab s
-  with Not_found -> 
-    errorlabstrm "Refiner.lookup_tactic"
-      (str"The tactic " ++ str s ++ str" is not installed")
-
-
 (* refiner r is a tactic applying the rule r *)
 
 let check_subproof_connection gl spfl =
@@ -201,6 +176,11 @@ let abstract_operation syntax semantics gls =
 let abstract_tactic_expr te tacfun gls =
   abstract_operation (Tactic te) tacfun gls	
 
+let abstract_tactic te = abstract_tactic_expr (Tacexpr.TacAtom (dummy_loc,te))
+
+let abstract_extended_tactic s args = 
+  abstract_tactic (Tacexpr.TacExtend (dummy_loc, s, args))
+
 let refiner = function
   | Prim pr as r ->
       let prim_fun = prim_refiner pr in
@@ -254,20 +234,6 @@ let local_Constraints gl = refiner Change_evars gl
 
 let norm_evar_tac = local_Constraints
 
-(*
-let vernac_tactic (s,args) =
-  let tacfun = lookup_tactic s args in
-  abstract_extra_tactic s args tacfun
-*)
-let abstract_tactic te = abstract_tactic_expr (Tacexpr.TacAtom (dummy_loc,te))
-
-let abstract_extended_tactic s args = 
-  abstract_tactic (Tacexpr.TacExtend (dummy_loc, s, args))
-
-let vernac_tactic (s,args) =
-  let tacfun = lookup_tactic s args in
-  abstract_extended_tactic s args tacfun
-
 (* [extract_open_proof : proof_tree -> constr * (int * constr) list]
   takes a (not necessarly complete) proof and gives a pair (pfterm,obl)
   where pfterm is the constr corresponding to the proof
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 097ff99a93..72afde93e0 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -32,10 +32,6 @@ val apply_sig_tac :
 
 type transformation_tactic = proof_tree -> (goal list * validation)
 
-val add_tactic             : string -> (closed_generic_argument list -> tactic) -> unit
-val overwriting_add_tactic : string -> (closed_generic_argument list -> tactic) -> unit
-val lookup_tactic          : string -> (closed_generic_argument list) -> tactic
-
 (*s Hiding the implementation of tactics. *)
 
 (* [abstract_tactic tac] hides the (partial) proof produced by [tac] under
@@ -46,7 +42,6 @@ val abstract_tactic_expr : tactic_expr -> tactic -> tactic
 val abstract_extended_tactic : string -> closed_generic_argument list -> tactic -> tactic
 
 val refiner : rule -> tactic
-val vernac_tactic : string * closed_generic_argument list -> tactic
 val frontier : transformation_tactic
 val list_pf : proof_tree -> goal list
 val unTAC : tactic -> goal sigma -> proof_tree sigma