Ajout 'Symmetry in Hyp'

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

9 files changed, 35 insertions, 12 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 3b7081012..c52a5888d 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -337,7 +337,8 @@ GEXTEND Gram
 
       (* Equivalence relations *)
       | IDENT "Reflexivity" -> TacReflexivity
-      | IDENT "Symmetry" -> TacSymmetry
+      | IDENT "Symmetry"; ido = OPT [ "in"; id = id_or_ltac_ref -> id ] -> 
+	  TacSymmetry ido
       | IDENT "Transitivity"; c = constr -> TacTransitivity c
 
       (* Conversion *)
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 0382a2fdb..817109a97 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -388,7 +388,7 @@ let rec pr_atom0 = function
   | TacAutoTDB None -> str "AutoTDB"
   | TacDestructConcl -> str "DConcl"
   | TacReflexivity -> str "Reflexivity"
-  | TacSymmetry -> str "Symmetry"
+  | TacSymmetry None -> str "Symmetry"
   | t -> str "(" ++ pr_atom1 t ++ str ")"
 
   (* Main tactic printer *)
@@ -530,7 +530,8 @@ and pr_atom1 = function
         brk (1,1) ++ pr_constr c ++ pr_clause pr_ident h)
 
   (* Equivalence relations *)
-  | (TacReflexivity | TacSymmetry) as x -> pr_atom0 x
+  | (TacReflexivity | TacSymmetry None) as x -> pr_atom0 x
+  | TacSymmetry (Some id) -> str "Symmetry " ++ pr_ident id
   | TacTransitivity c -> str "Transitivity" ++ pr_arg pr_constr c
 
 and pr_tactic_seq_body tl = 
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index f5ebd8fcf..697c78890 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -422,7 +422,7 @@ let rec mlexpr_of_atomic_tactic = function
 
   (* Equivalence relations *)
   | Tacexpr.TacReflexivity -> <:expr< Tacexpr.TacReflexivity >>
-  | Tacexpr.TacSymmetry -> <:expr< Tacexpr.TacSymmetry >>
+  | Tacexpr.TacSymmetry ido -> <:expr< Tacexpr.TacSymmetry $mlexpr_of_option mlexpr_of_hyp ido$ >>
   | Tacexpr.TacTransitivity c -> <:expr< Tacexpr.TacTransitivity $mlexpr_of_constr c$ >>
 
   (* Automation tactics *)
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 3098aceb3..75ebb2d28 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 *)
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 9024123f3..0e8725c6a 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -87,7 +87,7 @@ let h_change oc c cl  = abstract_tactic (TacChange (oc,c,cl)) (change oc c cl)
 
 (* Equivalence relations *)
 let h_reflexivity    = abstract_tactic TacReflexivity intros_reflexivity
-let h_symmetry       = abstract_tactic TacSymmetry intros_symmetry
+let h_symmetry c     = abstract_tactic (TacSymmetry c) (intros_symmetry c)
 let h_transitivity c =
   abstract_tactic (TacTransitivity c) (intros_transitivity c)
 
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index c01eca7f2..dba9908a9 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -95,7 +95,7 @@ val h_change          :
 
 (* Equivalence relations *)
 val h_reflexivity     : tactic
-val h_symmetry        : tactic
+val h_symmetry        : Tacticals.clause -> tactic
 val h_transitivity    : constr -> tactic
 
 val h_simplest_apply  : constr -> tactic 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index f92eefff0..84d8d84ac 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -623,7 +623,8 @@ let rec intern_atomic lf ist x =
 
   (* Equivalence relations *)
   | TacReflexivity -> TacReflexivity
-  | TacSymmetry -> TacSymmetry
+  | TacSymmetry idopt -> 
+      TacSymmetry (option_app (intern_hyp_or_metaid ist) idopt)
   | TacTransitivity c -> TacTransitivity (intern_constr ist c)
 
   (* For extensions *)
@@ -1644,7 +1645,7 @@ and interp_atomic ist gl = function
 
   (* Equivalence relations *)
   | TacReflexivity -> h_reflexivity
-  | TacSymmetry -> h_symmetry
+  | TacSymmetry c -> h_symmetry (option_app (interp_hyp ist gl) c)
   | TacTransitivity c -> h_transitivity (pf_interp_constr ist gl c)
 
   (* For extensions *)
@@ -1848,7 +1849,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
         subst_rawconstr subst c, cl)
 
   (* Equivalence relations *)
-  | TacReflexivity | TacSymmetry as x -> x
+  | TacReflexivity | TacSymmetry _ as x -> x
   | TacTransitivity c -> TacTransitivity (subst_rawconstr subst c)
 
   (* For extensions *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 126e61ec2..1b9f86023 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1606,7 +1606,26 @@ let symmetry gl =
 	      gl
 	end
 
-let intros_symmetry  = (tclTHEN intros symmetry)
+let symmetry_in id gl = 
+  let ctype = pf_type_of gl (mkVar id) in 
+  let sign,t = decompose_prod_assum ctype in
+  match match_with_equation t with
+    | None -> (* Do not deal with setoids yet *) 
+        error "The term provided does not end with an equation" 
+    | Some (hdcncl,args) -> 
+        let symccl = match args with 
+	  | [t1; c1; t2; c2] -> mkApp (hdcncl, [| t2; c2; t1; c1 |])
+          | [typ;c1;c2] -> mkApp (hdcncl, [| typ; c2; c1 |])
+          | [c1;c2]     -> mkApp (hdcncl, [| c2; c1 |])
+	  | _ -> assert false in
+	tclTHENS (cut (it_mkProd_or_LetIn symccl sign))
+	  [ intro_replacing id;
+            tclTHENLIST [ intros; symmetry; apply (mkVar id); assumption ] ]
+	  gl
+
+let intros_symmetry = function
+  | None -> tclTHEN intros symmetry
+  | Some id -> symmetry_in id
 
 (* Transitivity tactics *)
 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 5ff744e3f..38c31f015 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -222,7 +222,8 @@ val reflexivity                 : tactic
 val intros_reflexivity          : tactic
 
 val symmetry                    : tactic
-val intros_symmetry             : tactic
+val symmetry_in                 : identifier -> tactic
+val intros_symmetry             : clause -> tactic
 
 val transitivity                : constr -> tactic
 val intros_transitivity         : constr -> tactic