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

3 files changed, 43 insertions, 4 deletions

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index e9a204ada5..b803a878a6 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -155,7 +155,7 @@ let coq_MSCovariant = lazy(constant ["Setoid"] "MSCovariant")
 let coq_MSContravariant = lazy(constant ["Setoid"] "MSContravariant")
 
 let coq_singl = lazy(constant ["Setoid"] "singl")
-let coq_cons = lazy(constant ["Setoid"] "cons")
+let coq_cons = lazy(constant ["Setoid"] "necons")
 
 let coq_equality_morphism_of_asymmetric_areflexive_transitive_relation =
  lazy(constant ["Setoid"]
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index b6ad913f6e..2d98891167 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -248,6 +248,34 @@ let _ =
       Summary.survive_module = false;
       Summary.survive_section   = false }
 
+(* Tactics table (TacExtend). *)
+
+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")
+(*
+let vernac_tactic (s,args) =
+  let tacfun = lookup_tactic s args in
+  abstract_extended_tactic s args tacfun
+*)
 (* Interpretation of extra generic arguments *)
 type glob_sign = {
   ltacvars : identifier list * identifier list;
@@ -2062,7 +2090,10 @@ and interp_atomic ist gl = function
 
   (* For extensions *)
   | TacExtend (loc,opn,l) ->
-      fun gl -> vernac_tactic (opn,List.map (interp_genarg ist gl) l) gl
+      let tac = lookup_tactic opn in
+      fun gl ->
+        let args = List.map (interp_genarg ist gl) l in
+        abstract_extended_tactic opn args (tac args) gl
   | TacAlias (loc,_,l,(_,body)) -> fun gl ->
     let rec f x = match genarg_tag x with
     | IntArgType -> 
@@ -2143,7 +2174,7 @@ let interp_tac_gen lfun debug t gl =
       ltacvars = (List.map fst lfun, []); ltacrecvars = [];
       gsigma = project gl; genv = pf_env gl } t) gl
 
-let eval_tactic t = interp_tactic { lfun=[]; debug=get_debug() } t
+let eval_tactic t gls = interp_tactic { lfun=[]; debug=get_debug() } t gls
 
 let interp t = interp_tac_gen [] (get_debug()) t
 
@@ -2191,7 +2222,7 @@ let subst_induction_arg subst = function
   | ElimOnIdent id as x -> x
 
 let subst_and_short_name f (c,n) =
-  assert (n=None); (* since tacdef are strictly globalized *)
+(*  assert (n=None); *)(* since tacdef are strictly globalized *)
   (f c,None)
 
 let subst_or_var f =  function
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index f343bc9493..ca9b076d95 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -64,6 +64,14 @@ val add_tacdef :
   bool -> (identifier Util.located * raw_tactic_expr) list -> unit
 val add_primitive_tactic : string -> glob_tactic_expr -> unit
 
+(* Tactic extensions *)
+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
+
 (* Adds an interpretation function for extra generic arguments *)
 type glob_sign = {
   ltacvars : identifier list * identifier list;