Ajout 'Symmetry in Hyp'

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

5 files changed, 28 insertions, 7 deletions

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