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

4 files changed, 11 insertions, 31 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 97dfbfb1ed..b6cc55f617 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -46,7 +46,7 @@ and ct_COMMAND =
   | CT_coerce_THEOREM_GOAL_to_COMMAND of ct_THEOREM_GOAL
   | CT_abort of ct_ID_OPT_OR_ALL
   | CT_abstraction of ct_ID * ct_FORMULA * ct_INT_LIST
-  | CT_add_field of ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_BINDING_LIST
+  | CT_add_field of ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA_OPT
   | CT_add_natural_feature of ct_NATURAL_FEATURE * ct_ID
   | CT_addpath of ct_STRING * ct_ID_OPT
   | CT_arguments_scope of ct_ID * ct_ID_OPT_LIST
diff --git a/contrib/interface/debug_tac.ml4 b/contrib/interface/debug_tac.ml4
index e1b8e7125e..890bb3ce55 100644
--- a/contrib/interface/debug_tac.ml4
+++ b/contrib/interface/debug_tac.ml4
@@ -336,7 +336,7 @@ let debug_tac = function
 add_tactic "DebugTac" debug_tac;;
 *)
 
-Refiner.add_tactic "OnThen" on_then;;
+Tacinterp.add_tactic "OnThen" on_then;;
 
 let rec clean_path tac l = 
   match tac, l with
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 9c26c07111..fe227f9958 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -112,19 +112,12 @@ and fCOMMAND = function
    fFORMULA x2;
    fINT_LIST x3;
    fNODE "abstraction" 3
-| CT_add_field(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) ->
+| CT_add_field(x1, x2, x3, x4) ->
    fFORMULA x1;
    fFORMULA x2;
    fFORMULA x3;
-   fFORMULA x4;
-   fFORMULA x5;
-   fFORMULA x6;
-   fFORMULA x7;
-   fFORMULA x8;
-   fFORMULA x9;
-   fFORMULA x10;
-   fBINDING_LIST x11;
-   fNODE "add_field" 11
+   fFORMULA_OPT x4;
+   fNODE "add_field" 4
 | CT_add_natural_feature(x1, x2) ->
    fNATURAL_FEATURE x1;
    fID x2;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 292a428739..a7288de9a7 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1670,27 +1670,14 @@ let rec xlate_vernac =
 	CT_no_inline(CT_id_ne_list(loc_qualid_to_ct_ID fst,
 				List.map loc_qualid_to_ct_ID l2))
     | VernacExtend("Field", 
-		   [a;aplus;amult;aone;azero;aopp;aeq;ainv;fth;ainvl;minusdiv]) ->
+		   [fth;ainv;ainvl;div]) ->
 	(match List.map (fun v -> xlate_formula(out_gen rawwit_constr v))
-                   [a;aplus;amult;aone;azero;aopp;aeq;ainv;fth;ainvl]
+                   [fth;ainv;ainvl]
  	 with
-             [a1;aplus1;amult1;aone1;azero1;aopp1;aeq1;ainv1;fth1;ainvl1] ->
-	       let bind =
-		 match out_gen Field.rawwit_minus_div_arg minusdiv with
-		     None, None ->
-		       CT_binding_list[]
-		   | Some m, None ->
-		       CT_binding_list[
-			 CT_binding(CT_coerce_ID_to_ID_OR_INT (CT_ident "minus"), xlate_formula m)]
-		   | None, Some d ->
-		       CT_binding_list[
-			 CT_binding(CT_coerce_ID_to_ID_OR_INT (CT_ident "div"), xlate_formula d)]
-		   | Some m, Some d ->
-		       CT_binding_list[
-			 CT_binding(CT_coerce_ID_to_ID_OR_INT (CT_ident "minus"), xlate_formula m);
-			 CT_binding(CT_coerce_ID_to_ID_OR_INT (CT_ident "div"), xlate_formula d)] in
-		 CT_add_field(a1, aplus1, amult1, aone1, azero1, aopp1, aeq1,
-			      ainv1, fth1, ainvl1, bind)
+             [fth1;ainv1;ainvl1] ->
+	       let adiv1 =
+                 xlate_formula_opt (out_gen (wit_opt rawwit_constr) div) in
+	       CT_add_field(fth1, ainv1, ainvl1, adiv1)
 	   |_ -> assert false)
   | VernacExtend ("HintRewrite", o::f::([b]|[_;b] as args)) ->
       let orient = out_gen Extraargs.rawwit_orient o in