From 561081533ed884e3565fb71ca1c343bbc3fec448 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 19 Jun 2003 20:27:32 +0000
Subject: Ajout 'Symmetry in Hyp'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4186 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/interface/showproof.ml | 4 ++--
 contrib/interface/xlate.ml     | 3 ++-
 2 files changed, 4 insertions(+), 3 deletions(-)

(limited to 'contrib/interface')

diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index 9ff5675884..d33a41f98b 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -159,7 +159,7 @@ let rule_is_complex r =
    match r with
       Tactic (TacArg (Tacexp t),_) -> true  
    |  Tactic (TacAtom (_,TacAuto _), _) -> true
-   |  Tactic (TacAtom (_,TacSymmetry), _) -> true 
+   |  Tactic (TacAtom (_,TacSymmetry _), _) -> true 
    |_ -> false
 ;;
 
@@ -1143,7 +1143,7 @@ let is_equality_tac = function
 	 |"ERewriteParallel"|"ERewriteNormal"
 	 |"RewriteLR"|"RewriteRL"|"Replace"),_)
       | TacReduce _
-      | TacSymmetry | TacReflexivity
+      | TacSymmetry _ | TacReflexivity
       | TacExact _ | TacIntroPattern _ | TacIntroMove _ | TacAuto _)) -> true
   | _ -> false
 
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index c6baa0ecf9..c0ba10bddf 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -877,7 +877,8 @@ 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 -> CT_symmetry
+    | TacSymmetry None -> CT_symmetry
+    | TacSymmetry (Some _) -> xlate_error "TODO: Symmetry in"
     | TacTransitivity c -> CT_transitivity (xlate_formula c)
     | TacAssumption -> CT_assumption
     | TacExact c -> CT_exact (xlate_formula c)
-- 
cgit v1.2.3