adds a clause argument to symmetry

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

3 files changed, 5 insertions, 3 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 7106b5d65..bf138b394 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -581,7 +581,7 @@ and ct_TACTIC_COM =
   | CT_specialize of ct_INT_OPT * ct_FORMULA * ct_SPEC_LIST
   | CT_split of ct_SPEC_LIST
   | CT_superauto of ct_INT_OPT * ct_ID_LIST * ct_DESTRUCTING * ct_USINGTDB
-  | CT_symmetry
+  | CT_symmetry of ct_CLAUSE
   | CT_tac_double of ct_ID_OR_INT * ct_ID_OR_INT
   | CT_tacsolve of ct_TACTIC_COM * ct_TACTIC_COM list
   | CT_tactic_fun of ct_ID_UNIT_LIST * ct_TACTIC_COM
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index f3610f4d3..689ae2216 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -1428,7 +1428,9 @@ and fTACTIC_COM = function
    fDESTRUCTING x3;
    fUSINGTDB x4;
    fNODE "superauto" 4
-| CT_symmetry -> fNODE "symmetry" 0
+| CT_symmetry(x1) ->
+   fCLAUSE x1;
+   fNODE "symmetry" 1
 | CT_tac_double(x1, x2) ->
    fID_OR_INT x1;
    fID_OR_INT x2;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 9c91d930e..b2cb66d66 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -973,7 +973,7 @@ and xlate_tac =
       if b then CT_cutrewrite_lr (c, ctf_ID_OPT_SOME id)
       else CT_cutrewrite_lr (c, ctf_ID_OPT_SOME id)
     | TacReflexivity -> CT_reflexivity
-    | TacSymmetry _ -> xlate_error "TODO: Symmetry <clause>"
+    | TacSymmetry cls -> CT_symmetry(xlate_clause cls)
     | TacTransitivity c -> CT_transitivity (xlate_formula c)
     | TacAssumption -> CT_assumption
     | TacExact c -> CT_exact (xlate_formula c)