From 5f1e8b75c2f0d138e64cb57fbd7a3479f4b5d066 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 19 Jun 2003 20:19:00 +0000
Subject: Ajout 'Symmetry in Hyp'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4185 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/tacexpr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 3098aceb3a..75ebb2d286 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -152,7 +152,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
 
   (* Equivalence relations *)
   | TacReflexivity
-  | TacSymmetry
+  | TacSymmetry of 'id option
   | TacTransitivity of 'constr 
 
   (* For ML extensions *)
-- 
cgit v1.2.3