JMeq now treated as an equality by tactics.

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

3 files changed, 29 insertions, 18 deletions

diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 8e76487045..53ffa7a350 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -136,6 +136,12 @@ let coq_refl_rel1_pattern =
 let coq_refl_rel2_pattern =
   PProd (x, PMeta None, PApp (PMeta None, [|PRel 1; PRel 1|]))
 
+let coq_refl_reljm_pattern =
+PProd
+    (name_A, PMeta None,
+    PProd (x, PRel 1, PApp (PMeta None, [|PRel 2; PRel 1; PRel 2;PRel 1|])))
+  
+
 let match_with_equation t =
   let (hdapp,args) = decompose_app t in
   match (kind_of_term hdapp) with
@@ -145,7 +151,8 @@ let match_with_equation t =
         let nconstr = Array.length mip.mind_consnames in
 	if nconstr = 1 &&
            (is_matching coq_refl_rel1_pattern constr_types.(0) ||
-            is_matching coq_refl_rel1_pattern constr_types.(0)) 
+            is_matching coq_refl_rel2_pattern constr_types.(0) ||
+            is_matching coq_refl_reljm_pattern constr_types.(0)) 
         then 
 	  Some (hdapp,args)
         else 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5978e1070f..25ba260d43 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1548,6 +1548,7 @@ let symmetry gl =
 	    (apply (pf_parse_const gl ("sym_"^hdcncls)) gl)
           with  _ ->
             let symc = 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 
@@ -1583,16 +1584,18 @@ let transitivity t gl =
 	  try 
 	    apply_list [(pf_parse_const gl ("trans_"^hdcncls));t] gl 
           with  _ -> 
-            let eq1 = match args with 
-              | [typ;c1;c2] -> mkApp (hdcncl, [| typ; c1; t |])
-	      | [c1;c2]     -> mkApp (hdcncl, [| c1; t|])
+            let eq1, eq2 = match args with 
+	      | [typ1;c1;typ2;c2] -> let typt = pf_type_of gl t in
+                  ( mkApp(hdcncl, [| typ1; c1; typt ;t |]),
+		    mkApp(hdcncl, [| typt; t; typ2; c2 |]) )
+              | [typ;c1;c2] ->
+		  ( mkApp (hdcncl, [| typ; c1; t |]),
+		    mkApp (hdcncl, [| typ; t; c2 |]) )
+	      | [c1;c2]     ->
+		  ( mkApp (hdcncl, [| c1; t|]),
+		    mkApp (hdcncl, [| t; c2 |]) )
 	      | _ -> assert false 
 	    in
-            let eq2 = match args with 
-              | [typ;c1;c2] -> mkApp (hdcncl, [| typ; t; c2 |])
-	      | [c1;c2]     -> mkApp (hdcncl, [| t; c2 |])
-	      |  _ -> assert false 
-	    in
             tclTHENFIRST (cut eq2)
 	      (tclTHENFIRST (cut eq1)
                 (tclTHENLIST
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index a44edfbf27..47a20a63d9 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -14,34 +14,35 @@ Set Implicit Arguments.
 
 Inductive JMeq [A:Set;x:A] : (B:Set)B->Prop := 
 	JMeq_refl : (JMeq x x).
+Reset JMeq_ind.
 
 Hints Resolve JMeq_refl.
 
-Lemma JMeq_sym : (A,B:Set)(x:A)(y:B)(JMeq x y)->(JMeq y x).
+Lemma sym_JMeq : (A,B:Set)(x:A)(y:B)(JMeq x y)->(JMeq y x).
 NewDestruct 1; Trivial.
 Qed.
 
-Hints Immediate JMeq_sym.
+Hints Immediate sym_JMeq.
 
-Lemma JMeq_trans : (A,B,C:Set)(x:A)(y:B)(z:C)
+Lemma trans_JMeq : (A,B,C:Set)(x:A)(y:B)(z:C)
 	(JMeq x y)->(JMeq y z)->(JMeq x z).
 NewDestruct 1; Trivial.
 Qed.
 
 Axiom JMeq_eq : (A:Set)(x,y:A)(JMeq x y)->(x=y).
 
-Lemma JMeq_eq_ind : (A:Set)(x,y:A)(P:A->Prop)(P x)->(JMeq x y)->(P y).
+Lemma JMeq_ind : (A:Set)(x,y:A)(P:A->Prop)(P x)->(JMeq x y)->(P y).
 Intros A x y P H H'; Case JMeq_eq with 1:=H'; Trivial.
 Qed.
 
-Lemma JMeq_eq_rec : (A:Set)(x,y:A)(P:A->Set)(P x)->(JMeq x y)->(P y).
+Lemma JMeq_rec : (A:Set)(x,y:A)(P:A->Set)(P x)->(JMeq x y)->(P y).
 Intros A x y P H H'; Case JMeq_eq with 1:=H'; Trivial.
 Qed.
 
-Lemma JMeq_eq_ind_r : (A:Set)(x,y:A)(P:A->Prop)(P y)->(JMeq x y)->(P x).
-Intros A x y P H H'; Case JMeq_eq with 1:=(JMeq_sym H'); Trivial.
+Lemma JMeq_ind_r : (A:Set)(x,y:A)(P:A->Prop)(P y)->(JMeq x y)->(P x).
+Intros A x y P H H'; Case JMeq_eq with 1:=(sym_JMeq H'); Trivial.
 Qed.
 
-Lemma JMeq_eq_rec_r : (A:Set)(x,y:A)(P:A->Set)(P y)->(JMeq x y)->(P x).
-Intros A x y P H H'; Case JMeq_eq with 1:=(JMeq_sym H'); Trivial.
+Lemma JMeq_rec_r : (A:Set)(x,y:A)(P:A->Set)(P y)->(JMeq x y)->(P x).
+Intros A x y P H H'; Case JMeq_eq with 1:=(sym_JMeq H'); Trivial.
 Qed.