Added "etransitivity".

Added support for "injection" and "discriminate" on JMeq.

Seized the opportunity to update coqlib.ml and to rely more on it for
finding the equality lemmas.

Fixed typos in coqcompat.ml.
Propagated symmetry convert_concl fix to transitivity (see 11521).

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

23 files changed, 379 insertions, 251 deletions

diff --git a/CHANGES b/CHANGES
index 4c2ed82b8..0688f5246 100644
--- a/CHANGES
+++ b/CHANGES
@@ -24,6 +24,8 @@ Tactics
   variables and "**" for introducing all quantified variables and hypotheses.
 - Pattern Unification for existential variables activated in tactics and 
   new option "Unset Tactic Evars Pattern Unification" to deactivate it.
+- New tactic "etransitivity".
+- Support of JMeq for "injection" and "discriminate".
 
 Tactic Language
 
diff --git a/ide/coq.ml b/ide/coq.ml
index d81bb42f2..35feb59ed 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -523,14 +523,14 @@ let hyp_menu (env, sigma, ((coqident,ident),_,ast),(s,pr_ast)) =
     pr_ast
     ^".") ] @
 
-   (if is_equation ast then
+   (if is_equality_type ast then
       [ "discriminate "^ident, "discriminate "^ident^".";
 	"injection "^ident, "injection "^ident^"." ]
     else
       []) @
    
    (let _,t = splay_prod env sigma ast in
-    if is_equation t then 
+    if is_equality_type t then 
       [ "rewrite "^ident, "rewrite "^ident^".";
 	"rewrite <- "^ident, "rewrite <- "^ident^"." ]
     else
@@ -546,7 +546,7 @@ let hyp_menu (env, sigma, ((coqident,ident),_,ast),(s,pr_ast)) =
    ("inversion_clear "^ident^".")] 
 
 let concl_menu (_,_,concl,_) = 
-  let is_eq = is_equation concl in
+  let is_eq = is_equality_type concl in
   ["intro", "intro.";
    "intros", "intros.";
    "intuition","intuition." ] @
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 087a51982..e110ad00a 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -82,6 +82,8 @@ let init_reference dir s = gen_reference "Coqlib" ("Init"::dir) s
 
 let init_constant dir s = gen_constant "Coqlib" ("Init"::dir) s  
 
+let logic_constant dir s = gen_constant "Coqlib" ("Logic"::dir) s  
+
 let arith_dir = ["Coq";"Arith"]
 let arith_modules = [arith_dir]
 
@@ -107,9 +109,18 @@ let datatypes_id = id_of_string "Datatypes"
 
 let logic_module_name = ["Coq";"Init";"Logic"]
 let logic_module = make_dir logic_module_name
-let logic_type_module = make_dir ["Coq";"Init";"Logic_Type"]
-let datatypes_module = make_dir ["Coq";"Init";"Datatypes"]
-let arith_module = make_dir ["Coq";"Arith";"Arith"]
+
+let logic_type_module_name = ["Coq";"Init";"Logic_Type"]
+let logic_type_module = make_dir logic_type_module_name
+
+let datatypes_module_name = ["Coq";"Init";"Datatypes"]
+let datatypes_module = make_dir datatypes_module_name
+
+let arith_module_name = ["Coq";"Arith";"Arith"]
+let arith_module = make_dir arith_module_name
+
+let jmeq_module_name = ["Coq";"Logic";"JMeq"]
+let jmeq_module = make_dir jmeq_module_name
 
 (* TODO: temporary hack *)
 let make_kn dir id = Libnames.encode_kn dir id
@@ -145,9 +156,14 @@ let glob_false  = ConstructRef path_of_false
 
 (** Equality *)
 let eq_kn = make_kn logic_module (id_of_string "eq")
-
 let glob_eq = IndRef (eq_kn,0)
 
+let identity_kn = make_kn datatypes_module (id_of_string "identity")
+let glob_identity = IndRef (identity_kn,0)
+
+let jmeq_kn = make_kn jmeq_module (id_of_string "JMeq")
+let glob_jmeq = IndRef (jmeq_kn,0)
+
 type coq_sigma_data = {
   proj1 : constr;
   proj2 : constr;
@@ -185,18 +201,24 @@ let build_prod () =
     typ = init_constant ["Datatypes"] "prod" }
 
 (* Equalities *)
-type coq_leibniz_eq_data = {
+type coq_eq_data = {
   eq   : constr;
-  refl : constr;
   ind  : constr;
+  refl : constr;
+  sym  : constr;
+  trans: constr;
+  congr: constr }
+
+type coq_rewrite_data = {
   rrec : constr option;
-  rect : constr option;
-  congr: constr;
-  sym  : constr }
+  rect : constr option
+}
 
 let lazy_init_constant dir id = lazy (init_constant dir id)
+let lazy_logic_constant dir id = lazy (logic_constant dir id)
+
+(* Leibniz equality on Type *)
 
-(* Equality on Set *)
 let coq_eq_eq = lazy_init_constant ["Logic"] "eq"
 let coq_eq_refl = lazy_init_constant ["Logic"] "eq_refl"
 let coq_eq_ind = lazy_init_constant ["Logic"] "eq_ind"
@@ -204,17 +226,17 @@ let coq_eq_rec = lazy_init_constant ["Logic"] "eq_rec"
 let coq_eq_rect = lazy_init_constant ["Logic"] "eq_rect"
 let coq_eq_congr = lazy_init_constant ["Logic"] "f_equal"
 let coq_eq_sym  = lazy_init_constant ["Logic"] "eq_sym"
+let coq_eq_trans  = lazy_init_constant ["Logic"] "eq_trans"
 let coq_f_equal2 = lazy_init_constant ["Logic"] "f_equal2"
 
 let build_coq_eq_data () =
   let _ = check_required_library logic_module_name in {
   eq = Lazy.force coq_eq_eq;
-  refl = Lazy.force coq_eq_refl;
   ind = Lazy.force coq_eq_ind;
-  rrec = Some (Lazy.force coq_eq_rec);
-  rect = Some (Lazy.force coq_eq_rect);
-  congr = Lazy.force coq_eq_congr;
-  sym = Lazy.force coq_eq_sym }
+  refl = Lazy.force coq_eq_refl;
+  sym = Lazy.force coq_eq_sym;
+  trans = Lazy.force coq_eq_trans;
+  congr = Lazy.force coq_eq_congr }
 
 let build_coq_eq () = Lazy.force coq_eq_eq
 let build_coq_eq_sym () = Lazy.force coq_eq_sym
@@ -222,6 +244,26 @@ let build_coq_f_equal2 () = Lazy.force coq_f_equal2
 
 let build_coq_sym_eq = build_coq_eq_sym (* compatibility *)
 
+(* Heterogenous equality on Type *)
+
+let coq_jmeq_eq = lazy_logic_constant ["JMeq"] "JMeq"
+let coq_jmeq_refl = lazy_logic_constant ["JMeq"] "JMeq_refl"
+let coq_jmeq_ind = lazy_logic_constant ["JMeq"] "JMeq_ind"
+let coq_jmeq_rec = lazy_logic_constant ["JMeq"] "JMeq_rec"
+let coq_jmeq_rect = lazy_logic_constant ["JMeq"] "JMeq_rect"
+let coq_jmeq_sym  = lazy_logic_constant ["JMeq"] "JMeq_sym"
+let coq_jmeq_congr  = lazy_logic_constant ["JMeq"] "JMeq_congr"
+let coq_jmeq_trans  = lazy_logic_constant ["JMeq"] "JMeq_trans"
+
+let build_coq_jmeq_data () =
+  let _ = check_required_library jmeq_module_name in {
+  eq = Lazy.force coq_jmeq_eq;
+  ind = Lazy.force coq_jmeq_ind;
+  refl = Lazy.force coq_jmeq_refl;
+  sym = Lazy.force coq_jmeq_sym;
+  trans = Lazy.force coq_jmeq_trans;
+  congr = Lazy.force coq_jmeq_congr }
+
 (* Specif *)
 let coq_sumbool  = lazy_init_constant ["Specif"] "sumbool"
 
@@ -235,15 +277,16 @@ let coq_identity_rec = lazy_init_constant ["Datatypes"] "identity_rec"
 let coq_identity_rect = lazy_init_constant ["Datatypes"] "identity_rect"
 let coq_identity_congr = lazy_init_constant ["Logic_Type"] "identity_congr"
 let coq_identity_sym = lazy_init_constant ["Logic_Type"] "identity_sym"
+let coq_identity_trans = lazy_init_constant ["Logic_Type"] "identity_trans"
 
-let build_coq_identity_data () = {
+let build_coq_identity_data () =
+  let _ = check_required_library datatypes_module_name in {
   eq = Lazy.force coq_identity_eq;
-  refl = Lazy.force coq_identity_refl;
   ind = Lazy.force coq_identity_ind;
-  rrec = Some (Lazy.force coq_identity_rec);
-  rect = Some (Lazy.force coq_identity_rect);
-  congr = Lazy.force coq_identity_congr;
-  sym = Lazy.force coq_identity_sym }
+  refl = Lazy.force coq_identity_refl;
+  sym = Lazy.force coq_identity_sym;
+  trans = Lazy.force coq_identity_trans;
+  congr = Lazy.force coq_identity_congr }
 
 (* The False proposition *)
 let coq_False  = lazy_init_constant ["Logic"] "False"
@@ -281,7 +324,8 @@ let build_coq_iff_right_proj () = Lazy.force coq_iff_right_proj
 
 (* The following is less readable but does not depend on parsing *)
 let coq_eq_ref      = lazy (init_reference ["Logic"] "eq")
-let coq_identity_ref     = lazy (init_reference ["Datatypes"] "identity")
+let coq_identity_ref = lazy (init_reference ["Datatypes"] "identity")
+let coq_jmeq_ref     = lazy (gen_reference "Coqlib" ["Logic";"JMeq"] "JMeq")
 let coq_existS_ref  = lazy (anomaly "use coq_existT_ref")
 let coq_existT_ref  = lazy (init_reference ["Specif"] "existT")
 let coq_not_ref     = lazy (init_reference ["Logic"] "not")
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 7e13b1b1e..5b550a86b 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -76,6 +76,8 @@ val glob_false : global_reference
 
 (* Equality *)
 val glob_eq : global_reference
+val glob_identity : global_reference
+val glob_jmeq : global_reference
 
 (*s Constructions and patterns related to Coq initial state are unknown
    at compile time. Therefore, we can only provide methods to build
@@ -104,22 +106,23 @@ val build_sigma_type : coq_sigma_data delayed
 (* Non-dependent pairs in Set from Datatypes *)
 val build_prod : coq_sigma_data delayed
 
-type coq_leibniz_eq_data = {
+type coq_eq_data = {
   eq   : constr;
-  refl : constr;
   ind  : constr;
-  rrec : constr option;
-  rect : constr option;
-  congr: constr;
-  sym  : constr }
+  refl : constr;
+  sym  : constr;
+  trans: constr;
+  congr: constr }
 
-val build_coq_eq_data : coq_leibniz_eq_data delayed
-val build_coq_identity_data : coq_leibniz_eq_data delayed
+val build_coq_eq_data : coq_eq_data delayed
+val build_coq_identity_data : coq_eq_data delayed
+val build_coq_jmeq_data : coq_eq_data delayed
 
 val build_coq_eq       : constr delayed (* = [(build_coq_eq_data()).eq] *)
 val build_coq_eq_sym   : constr delayed (* = [(build_coq_eq_data()).sym] *)
 val build_coq_f_equal2 : constr delayed
 
+
 (* Specif *)
 val build_coq_sumbool : constr delayed
 
@@ -150,6 +153,7 @@ val build_coq_ex : constr delayed
 
 val coq_eq_ref : global_reference lazy_t
 val coq_identity_ref : global_reference lazy_t
+val coq_jmeq_ref : global_reference lazy_t
 val coq_existS_ref : global_reference lazy_t
 val coq_existT_ref : global_reference lazy_t
 val coq_not_ref : global_reference lazy_t
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index c0a3f2e77..d5d32ce5b 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -616,7 +616,8 @@ GEXTEND Gram
       (* Equivalence relations *)
       | IDENT "reflexivity" -> TacReflexivity
       | IDENT "symmetry"; cl = clause_dft_concl -> TacSymmetry cl
-      | IDENT "transitivity"; c = constr -> TacTransitivity c
+      | IDENT "transitivity"; c = constr -> TacTransitivity (Some c)
+      | IDENT "etransitivity" -> TacTransitivity None
 
       (* Equality and inversion *)
       | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ","; 
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 357a572be..bdd9241e3 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -844,7 +844,8 @@ and pr_atom1 = function
   (* Equivalence relations *)
   | TacReflexivity as x -> pr_atom0 x
   | TacSymmetry cls -> str "symmetry " ++ pr_clauses pr_ident cls
-  | TacTransitivity c -> str "transitivity" ++ pr_constrarg c
+  | TacTransitivity (Some c) -> str "transitivity" ++ pr_constrarg c
+  | TacTransitivity None -> str "etransitivity"
 
   (* Equality and inversion *)
   | TacRewrite (ev,l,cl,by) -> 
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index a494738f9..606b652c2 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -413,7 +413,7 @@ let rec mlexpr_of_atomic_tactic = function
   (* Equivalence relations *)
   | Tacexpr.TacReflexivity -> <:expr< Tacexpr.TacReflexivity >>
   | Tacexpr.TacSymmetry ido -> <:expr< Tacexpr.TacSymmetry $mlexpr_of_clause ido$ >>
-  | Tacexpr.TacTransitivity c -> <:expr< Tacexpr.TacTransitivity $mlexpr_of_constr c$ >>
+  | Tacexpr.TacTransitivity c -> <:expr< Tacexpr.TacTransitivity $mlexpr_of_option mlexpr_of_constr c$ >>
 
   (* Automation tactics *)
   | Tacexpr.TacAuto (n,lems,l) ->
diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4
index 93de6118b..c9b993690 100644
--- a/plugins/field/field.ml4
+++ b/plugins/field/field.ml4
@@ -154,10 +154,12 @@ END
 (* Guesses the type and calls field_gen with the right theory *)
 let field g =
   Coqlib.check_required_library ["Coq";"field";"LegacyField"];
-  let typ = 
-    match Hipattern.match_with_equation (pf_concl g) with
-      | Some (eq,t::args) when eq = (Coqlib.build_coq_eq_data()).Coqlib.eq -> t
-      | _ -> error "The statement is not built from Leibniz' equality" in
+  let typ =
+    try match Hipattern.match_with_equation (pf_concl g) with
+      | _,_,Hipattern.PolymorphicLeibnizEq (t,_,_) -> t
+      | _ -> raise Exit
+    with Hipattern.NoEquationFound | Exit ->
+      error "The statement is not built from Leibniz' equality" in
   let th = VConstr (lookup (pf_env g) typ) in
   (interp_tac_gen [(id_of_string "FT",th)] [] (get_debug ())
     <:tactic< match goal with |- (@eq _ _ _) => field_gen FT end >>) g
diff --git a/plugins/interface/depends.ml b/plugins/interface/depends.ml
index 445b193f8..9e649a5a2 100644
--- a/plugins/interface/depends.ml
+++ b/plugins/interface/depends.ml
@@ -357,7 +357,8 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of
     (* Equivalence relations *)
     | TacReflexivity
     | TacSymmetry     _ -> acc
-    | TacTransitivity c -> depends_of_'constr c acc
+    | TacTransitivity (Some c) -> depends_of_'constr c acc
+    | TacTransitivity None -> acc
 
     (* Equality and inversion *)
     | TacRewrite (_,cbl,_,_) -> list_union_map (o depends_of_'constr_with_bindings (fun (_,_,x)->x)) cbl acc
diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml
index bff8cae26..9629fa923 100644
--- a/plugins/interface/xlate.ml
+++ b/plugins/interface/xlate.ml
@@ -1066,7 +1066,8 @@ and xlate_tac =
 		(out_gen (wit_list1 rawwit_ident) l)))
     | TacReflexivity -> CT_reflexivity
     | TacSymmetry cls -> CT_symmetry(xlate_clause cls)
-    | TacTransitivity c -> CT_transitivity (xlate_formula c)
+    | TacTransitivity (Some c) -> CT_transitivity (xlate_formula c)
+    | TacTransitivity None -> xlate_error "TODO: etransitivity"
     | TacAssumption -> CT_assumption
     | TacExact c -> CT_exact (xlate_formula c)
     | TacExactNoCheck c -> CT_exact_no_check (xlate_formula c)
diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml
index adcf51fe8..6dcc1e872 100644
--- a/plugins/ring/ring.ml
+++ b/plugins/ring/ring.ml
@@ -892,16 +892,18 @@ let polynom lc gl =
       do "Ring c1 c2 ... cn" and then try to apply the simplification
       theorems declared for the relation *)
     | [] ->
-	(match Hipattern.match_with_equation (pf_concl gl) with
-	   | Some (eq,t::args) ->
+	(try 
+	  match Hipattern.match_with_equation (pf_concl gl) with
+	   | _,_,Hipattern.PolymorphicLeibnizEq (t,c1,c2) ->
 	       let th = guess_theory t in
-	       if List.exists 
-		 (fun c1 -> not (safe_pf_conv_x gl t (pf_type_of gl c1))) args
-	       then 
-		 errorlabstrm "Ring :"
-		   (str" All terms must have the same type");
-	       (tclTHEN (raw_polynom th None args) (guess_eq_tac th)) gl
-	   | _ -> (match match_with_equiv (pf_concl gl) with
+	       (tclTHEN (raw_polynom th None [c1;c2]) (guess_eq_tac th)) gl
+	   | _,_,Hipattern.HeterogenousEq (t1,c1,t2,c2) 
+	       when safe_pf_conv_x gl t1 t2 ->
+	       let th = guess_theory t1 in
+	       (tclTHEN (raw_polynom th None [c1;c2]) (guess_eq_tac th)) gl
+	   | _ -> raise Exit
+	  with Hipattern.NoEquationFound | Exit ->
+	          (match match_with_equiv (pf_concl gl) with
 		     | Some (equiv, c1::args) ->
 			 let t = (pf_type_of gl c1) in
 			 let th = (guess_theory t) in
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 6b153fa10..65b330c3d 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -208,7 +208,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   (* Equivalence relations *)
   | TacReflexivity
   | TacSymmetry of 'id gclause
-  | TacTransitivity of 'constr 
+  | TacTransitivity of 'constr option
 
   (* Equality and inversion *)
   | TacRewrite of 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index ce0677cae..101e7ef8c 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -632,10 +632,9 @@ let apply_on_clause (f,t) clause =
      | _  -> errorlabstrm "" (str "Ill-formed clause applicator.")) in
   clenv_fchain argmv f_clause clause
 
-let discr_positions env sigma (lbeq,(t,t1,t2)) eq_clause cpath dirn sort =
+let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort =
   let e = next_ident_away eq_baseid (ids_of_context env) in
   let e_env = push_named (e,None,t) env in
-  let eqn = mkApp(lbeq.eq,[|t;t1;t2|]) in
   let discriminator =
     build_discriminator sigma e_env dirn (mkVar e) sort cpath in
   let (pf, absurd_term) = discrimination_pf e (t,t1,t2) discriminator lbeq in
@@ -645,8 +644,8 @@ let discr_positions env sigma (lbeq,(t,t1,t2)) eq_clause cpath dirn sort =
   tclTHENS (cut_intro absurd_term)
     [onLastHypId gen_absurdity; refine pf]
 
-let discrEq (lbeq,(t,t1,t2) as u) eq_clause gls =
-  let sigma =  eq_clause.evd in
+let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause gls =
+  let sigma = eq_clause.evd in
   let env = pf_env gls in
   match find_positions env sigma t1 t2 with
     | Inr _ ->
@@ -655,19 +654,26 @@ let discrEq (lbeq,(t,t1,t2) as u) eq_clause gls =
 	let sort = pf_apply get_type_of gls (pf_concl gls) in 
 	discr_positions env sigma u eq_clause cpath dirn sort gls
 
+let extract_main_eq_args gl = function
+  | MonomorphicLeibnizEq (e1,e2) -> let t = pf_type_of gl e1 in (t,e1,e2)
+  | PolymorphicLeibnizEq (t,e1,e2) -> (t,e1,e2)
+  | HeterogenousEq (t1,e1,t2,e2) ->
+      if pf_conv_x gl t1 t2 then (t1,e1,e2)
+      else error"Don't know what to do with JMeq on arguments not of same type."
+
 let onEquality with_evars tac (c,lbindc) gls =
   let t = pf_type_of gls c in
   let t' = try snd (pf_reduce_to_quantified_ind gls t) with UserError _ -> t in
   let eq_clause = make_clenv_binding gls (c,t') lbindc in
   let eq_clause' = clenv_pose_dependent_evars with_evars eq_clause in
   let eqn = clenv_type eq_clause' in
-  let eq =
+  let eq,eq_args =
     try find_eq_data_decompose eqn
     with PatternMatchingFailure ->
       errorlabstrm "" (str"No primitive equality found.") in
   tclTHEN
     (Refiner.tclEVARS eq_clause'.evd) 
-    (tac eq eq_clause') gls
+    (tac (eq,eqn,extract_main_eq_args gls eq_args) eq_clause') gls
 
 let onNegatedEquality with_evars tac gls =
   let ccl = pf_concl gls in
@@ -688,7 +694,9 @@ let discr with_evars = onEquality with_evars discrEq
 let discrClause with_evars = onClause (discrSimpleClause with_evars)
 
 let discrEverywhere with_evars = 
+(*
   tclORELSE
+*)
     (if !discr_do_intro then
       (tclTHEN
 	(tclREPEAT introf) 
@@ -696,9 +704,9 @@ let discrEverywhere with_evars =
           (fun id -> tclCOMPLETE (discr with_evars (mkVar id,NoBindings)))))
      else (* <= 8.2 compat *)
        Tacticals.tryAllHypsAndConcl (discrSimpleClause with_evars))
-    (fun gls -> 
+(*    (fun gls -> 
        errorlabstrm "DiscrEverywhere" (str"No discriminable equalities."))
-
+*)
 let discr_tac with_evars = function
   | None -> discrEverywhere with_evars
   | Some c -> onInductionArg (discr with_evars) c
@@ -926,7 +934,7 @@ let simplify_args env sigma t =
     | eq, [t1;c1;t2;c2] -> applist (eq,[t1;nf env sigma c1;t2;nf env sigma c2])
     | _ -> t
 
-let inject_at_positions env sigma (eq,(t,t1,t2)) eq_clause posns =
+let inject_at_positions env sigma (eq,_,(t,t1,t2)) eq_clause posns =
   let e = next_ident_away eq_baseid (ids_of_context env) in
   let e_env = push_named (e,None,t) env in
   let injectors =
@@ -951,8 +959,8 @@ let inject_at_positions env sigma (eq,(t,t1,t2)) eq_clause posns =
 exception Not_dep_pair
 
 
-let injEq ipats (eq,(t,t1,t2)) eq_clause =
-  let sigma =  eq_clause.evd in
+let injEq ipats (eq,_,(t,t1,t2) as u) eq_clause =
+  let sigma = eq_clause.evd in
   let env = eq_clause.env in
   match find_positions env sigma t1 t2 with
     | Inl _ ->
@@ -1000,7 +1008,7 @@ let injEq ipats (eq,(t,t1,t2)) eq_clause =
             ) else (raise Not_dep_pair) 
         ) with _ ->
 	tclTHEN
-	  (inject_at_positions env sigma (eq,(t,t1,t2)) eq_clause posns)
+	  (inject_at_positions env sigma u eq_clause posns)
 	  (intros_pattern no_move ipats)
 
 let inj ipats with_evars = onEquality with_evars (injEq ipats)
@@ -1012,7 +1020,7 @@ let injClause ipats with_evars = function
 let injConcl gls  = injClause [] false None gls
 let injHyp id gls = injClause [] false (Some (ElimOnIdent (dummy_loc,id))) gls
 
-let decompEqThen ntac (lbeq,(t,t1,t2) as u) clause gls =
+let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause gls =
   let sort = pf_apply get_type_of gls (pf_concl gls) in 
   let sigma =  clause.evd in
   let env = pf_env gls in 
@@ -1023,8 +1031,7 @@ let decompEqThen ntac (lbeq,(t,t1,t2) as u) clause gls =
         ntac 0 gls
     | Inr posns ->
 	tclTHEN
-	  (inject_at_positions env sigma (lbeq,(t,t1,t2)) clause
-	    (List.rev posns))
+	  (inject_at_positions env sigma u clause (List.rev posns))
 	  (ntac (List.length posns))
 	  gls
 
@@ -1034,14 +1041,26 @@ let dEqThen with_evars ntac = function
 
 let dEq with_evars = dEqThen with_evars (fun x -> tclIDTAC)
 
+let swap_equality_args = function
+  | MonomorphicLeibnizEq (e1,e2) -> [e2;e1]
+  | PolymorphicLeibnizEq (t,e1,e2) -> [t;e2;e1]
+  | HeterogenousEq (t1,e1,t2,e2) -> [t2;e2;t1;e1]
+
+let get_equality_args = function
+  | MonomorphicLeibnizEq (e1,e2) -> [e1;e2]
+  | PolymorphicLeibnizEq (t,e1,e2) -> [t;e1;e2]
+  | HeterogenousEq (t1,e1,t2,e2) -> [t1;e1;t2;e2]
+
 let swap_equands gls eqn =
-  let (lbeq,(t,e1,e2)) = find_eq_data_decompose eqn in 
-  applist(lbeq.eq,[t;e2;e1])
+  let (lbeq,eq_args) = find_eq_data_decompose eqn in 
+  applist(lbeq.eq,swap_equality_args eq_args)
 
 let swapEquandsInConcl gls =
-  let (lbeq,(t,e1,e2)) = find_eq_data_decompose (pf_concl gls) in
+  let (lbeq,eq_args) = find_eq_data_decompose (pf_concl gls) in
   let sym_equal = lbeq.sym in
-  refine (applist(sym_equal,[t;e2;e1;Evarutil.mk_new_meta()])) gls
+  refine
+    (applist(sym_equal,(swap_equality_args eq_args@[Evarutil.mk_new_meta()])))
+    gls
 
 (* Refine from [|- P e2] to [|- P e1] and [|- e1=e2:>t] (body is P (Rel 1)) *)
 
@@ -1102,12 +1121,13 @@ let subst_tuple_term env sigma dep_pair b =
       (fun (e,t) body -> lambda_create env (t,subst_term e body)) e_list b in
   beta_applist(abst_B,proj_list)
 
-(* Comme "replace" mais decompose les egalites dependantes *)
+(* Like "replace" but decompose dependent equalities *)
 
 exception NothingToRewrite
 
 let cutSubstInConcl_RL eqn gls =
-  let (lbeq,(t,e1,e2 as eq)) = find_eq_data_decompose eqn in
+  let (lbeq,eq_args) = find_eq_data_decompose eqn in
+  let (t,e1,e2 as eq) = extract_main_eq_args gls eq_args in
   let body = pf_apply subst_tuple_term gls e2 (pf_concl gls) in
   if not (dependent (mkRel 1) body) then raise NothingToRewrite;
   bareRevSubstInConcl lbeq body eq gls
@@ -1125,7 +1145,8 @@ let cutSubstInConcl_LR eqn gls =
 let cutSubstInConcl l2r =if l2r then cutSubstInConcl_LR else cutSubstInConcl_RL
 
 let cutSubstInHyp_LR eqn id gls =
-  let (lbeq,(t,e1,e2 as eq)) = find_eq_data_decompose eqn in 
+  let (lbeq,eq_args) = find_eq_data_decompose eqn in 
+  let (t,e1,e2 as eq) = extract_main_eq_args gls eq_args in
   let body = pf_apply subst_tuple_term gls e1 (pf_get_hyp_typ gls id) in
   if not (dependent (mkRel 1) body) then raise NothingToRewrite;
   cut_replacing id (subst1 e2 body)
@@ -1208,9 +1229,9 @@ let unfold_body x gl =
 exception FoundHyp of (identifier * constr * bool)
 
 (* tests whether hyp [c] is [x = t] or [t = x], [x] not occuring in [t] *)
-let is_eq_x x (id,_,c) =
+let is_eq_x gl x (id,_,c) =
   try
-    let (_,lhs,rhs) = snd (find_eq_data_decompose c) in
+    let (_,lhs,rhs) = extract_main_eq_args gl (snd(find_eq_data_decompose c)) in
     if (x = lhs) && not (occur_term x rhs) then raise (FoundHyp (id,rhs,true));
     if (x = rhs) && not (occur_term x lhs) then raise (FoundHyp (id,lhs,false))
   with PatternMatchingFailure ->
@@ -1226,7 +1247,7 @@ let subst_one x gl =
   (* Find a non-recursive definition for x *)
   let (hyp,rhs,dir) = 
     try
-      let test hyp _ = is_eq_x varx hyp in
+      let test hyp _ = is_eq_x gl varx hyp in
       Sign.fold_named_context test ~init:() hyps;
       errorlabstrm "Subst"
         (str "Cannot find any non-recursive equality over " ++ pr_id x ++
@@ -1274,7 +1295,7 @@ let subst ids = tclTHEN tclNORMEVAR (tclMAP subst_one ids)
 let subst_all gl =
   let test (_,c) =
     try
-      let (_,x,y) = snd (find_eq_data_decompose c) in
+      let (_,x,y) = extract_main_eq_args gl (snd (find_eq_data_decompose c)) in
       (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
       if eq_constr x y then failwith "caught";
       match kind_of_term x with Var x -> x | _ -> 
@@ -1291,19 +1312,19 @@ let subst_all gl =
 
 let cond_eq_term_left c t gl =
   try
-    let (_,x,_) = snd (find_eq_data_decompose t) in
+    let (_,x,_) = extract_main_eq_args gl (snd (find_eq_data_decompose t)) in
     if pf_conv_x gl c x then true else failwith "not convertible"
   with PatternMatchingFailure -> failwith "not an equality"
 
 let cond_eq_term_right c t gl = 
   try
-    let (_,_,x) = snd (find_eq_data_decompose t) in
+    let (_,_,x) = extract_main_eq_args gl (snd (find_eq_data_decompose t)) in
     if pf_conv_x gl c x then false else failwith "not convertible"
   with PatternMatchingFailure -> failwith "not an equality"
 
 let cond_eq_term c t gl = 
   try
-    let (_,x,y) = snd (find_eq_data_decompose t) in
+    let (_,x,y) = extract_main_eq_args gl (snd (find_eq_data_decompose t)) in
     if pf_conv_x gl c x then true 
     else if pf_conv_x gl c y then false
     else failwith "not convertible"
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index b85491c57..65a56100b 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -128,7 +128,8 @@ let h_change oc c cl =
 let h_reflexivity    = abstract_tactic TacReflexivity intros_reflexivity
 let h_symmetry c     = abstract_tactic (TacSymmetry c) (intros_symmetry c)
 let h_transitivity c =
-  abstract_tactic (TacTransitivity (inj_open c)) (intros_transitivity c)
+  abstract_tactic (TacTransitivity (Option.map inj_open c))
+    (intros_transitivity c)
 
 let h_simplest_apply c  = h_apply false false [inj_open c,NoBindings]
 let h_simplest_eapply c = h_apply false true [inj_open c,NoBindings]
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 5aafb91a0..f5b2dbb55 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -113,7 +113,7 @@ val h_change          :
 (* Equivalence relations *)
 val h_reflexivity     : tactic
 val h_symmetry        : Tacticals.clause -> tactic
-val h_transitivity    : constr -> tactic
+val h_transitivity    : constr option -> tactic
 
 val h_simplest_apply  : constr -> tactic 
 val h_simplest_eapply : constr -> tactic 
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index 7086e4421..0b81a492a 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -219,28 +219,47 @@ let is_unit_type t =
    inductive binary relation R, so that R has only one constructor
    establishing its reflexivity.  *)
 
-let coq_refl_rel1_pattern  = PATTERN [ forall A:_, forall x:A, _ A x x ]
-let coq_refl_rel2_pattern  = PATTERN [ forall x:_, _ x x ]
-let coq_refl_reljm_pattern = PATTERN [ forall A:_, forall x:A, _ A x A x ]
+type equation_kind =
+  | MonomorphicLeibnizEq of constr * constr
+  | PolymorphicLeibnizEq of constr * constr * constr
+  | HeterogenousEq of constr * constr * constr * constr
+
+exception NoEquationFound
+
+let coq_refl_leibniz1_pattern = PATTERN [ forall x:_, _ x x ]
+let coq_refl_leibniz2_pattern = PATTERN [ forall A:_, forall x:A, _ A x x ]
+let coq_refl_jm_pattern       = PATTERN [ forall A:_, forall x:A, _ A x A x ]
+
+open Libnames
 
 let match_with_equation t =
-  let (hdapp,args) = decompose_app t in
-  match (kind_of_term hdapp) with
-    | Ind ind -> 
+  if not (isApp t) then raise NoEquationFound;
+  let (hdapp,args) = destApp t in
+  match kind_of_term hdapp with
+  | Ind ind ->
+      if IndRef ind = glob_eq then
+	Some (build_coq_eq_data()),hdapp,
+	PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
+      else if IndRef ind = glob_identity then
+	Some (build_coq_identity_data()),hdapp,
+	PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
+      else if IndRef ind = glob_jmeq then
+	Some (build_coq_jmeq_data()),hdapp,
+	HeterogenousEq(args.(0),args.(1),args.(2),args.(3))
+      else
         let (mib,mip) = Global.lookup_inductive ind in
         let constr_types = mip.mind_nf_lc in 
         let nconstr = Array.length mip.mind_consnames in
-	if nconstr = 1 &&
-           (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 
-	  None
-    | _ -> None
-
-let is_equation t = op2bool (match_with_equation  t)
+	if nconstr = 1 then
+          if is_matching coq_refl_leibniz1_pattern constr_types.(0) then
+	    None, hdapp, MonomorphicLeibnizEq(args.(0),args.(1))
+	  else if is_matching coq_refl_leibniz2_pattern constr_types.(0) then
+	    None, hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
+	  else if is_matching coq_refl_jm_pattern constr_types.(0) then
+	    None, hdapp, HeterogenousEq(args.(0),args.(1),args.(2),args.(3))
+	  else raise NoEquationFound
+        else raise NoEquationFound
+    | _ -> raise NoEquationFound
 
 let match_with_equality_type t =
   let (hdapp,args) = decompose_app t in
@@ -255,6 +274,8 @@ let match_with_equality_type t =
 	  None
     | _ -> None
 
+let is_equality_type t = op2bool (match_with_equality_type t)
+
 let coq_arrow_pattern = PATTERN [ ?X1 -> ?X2 ]
 
 let match_arrow_pattern t =
@@ -333,16 +354,22 @@ let rec first_match matcher = function
 let coq_eq_pattern_gen eq = lazy PATTERN [ %eq ?X1 ?X2 ?X3 ]
 let coq_eq_pattern = coq_eq_pattern_gen coq_eq_ref
 let coq_identity_pattern = coq_eq_pattern_gen coq_identity_ref
+let coq_jmeq_pattern = lazy PATTERN [ %coq_jmeq_ref ?X1 ?X2 ?X3 ?X4 ]
 
 let match_eq eqn eq_pat =
-  match matches (Lazy.force eq_pat) eqn with
+  let pat = try Lazy.force eq_pat with _ -> raise PatternMatchingFailure in
+  match matches pat eqn with
     | [(m1,t);(m2,x);(m3,y)] ->
 	assert (m1 = meta1 & m2 = meta2 & m3 = meta3);
-	(t,x,y)
-    | _ -> anomaly "match_eq: an eq pattern should match 3 terms"
+	PolymorphicLeibnizEq (t,x,y)
+    | [(m1,t);(m2,x);(m3,t');(m4,x')] ->
+	assert (m1 = meta1 & m2 = meta2 & m3 = meta3 & m4 = meta4);
+	HeterogenousEq (t,x,t',x')
+    | _ -> anomaly "match_eq: an eq pattern should match 3 or 4 terms"
 
 let equalities =
   [coq_eq_pattern, build_coq_eq_data;
+   coq_jmeq_pattern, build_coq_jmeq_data;
    coq_identity_pattern, build_coq_identity_data]
 
 let find_eq_data_decompose eqn = (* fails with PatternMatchingFailure *)
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 3418dd208..5be8b2026 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -16,6 +16,7 @@ open Sign
 open Evd
 open Pattern
 open Proof_trees
+open Coqlib
 (*i*)
 
 (*s Given a term with second-order variables in it,
@@ -81,11 +82,9 @@ val is_unit_or_eq_type     : testing_function
 (* type with only one constructor and no arguments, no indices *)
 val is_unit_type           : testing_function 
 
-val match_with_equation    : (constr * constr list) matching_function
-val is_equation            : testing_function 
-
 (* type with only one constructor, no arguments and at least one dependency *)
 val match_with_equality_type : (constr * constr list) matching_function
+val is_equality_type       : testing_function
 
 val match_with_nottype     : (constr * constr) matching_function
 val is_nottype             : testing_function 
@@ -110,14 +109,23 @@ val is_nodep_ind           : testing_function
 val match_with_sigma_type   : (constr * constr list) matching_function	  
 val is_sigma_type           : testing_function 
 
-(***** Destructing patterns bound to some theory *)
+(* Recongnize inductive relation defined by reflexivity *)
 
-open Coqlib
+type equation_kind =
+  | MonomorphicLeibnizEq of constr * constr
+  | PolymorphicLeibnizEq of constr * constr * constr
+  | HeterogenousEq of constr * constr * constr * constr
+
+exception NoEquationFound
+
+val match_with_equation:
+  constr -> coq_eq_data option * constr * equation_kind
+
+(***** Destructing patterns bound to some theory *)
 
 (* Match terms [(eq A t u)] or [(identity A t u)] *)
 (* Returns associated lemmas and [A,t,u] *)
-val find_eq_data_decompose : constr -> 
-  coq_leibniz_eq_data * (constr * constr * constr)
+val find_eq_data_decompose : constr -> coq_eq_data * equation_kind
 
 (* Match a term of the form [(existT A P t p)] *)
 (* Returns associated lemmas and [A,P,t,p] *)
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 52f10d46c..43ae99203 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1390,9 +1390,8 @@ let setoid_proof gl ty fn fallback =
       let evm, car = project gl, pf_type_of gl args.(0) in
 	fn env evm car rel gl
     with e -> 
-      match fallback gl with
-      | Some tac -> tac gl
-      | None -> 
+      try fallback gl
+      with Hipattern.NoEquationFound ->
 	  match e with
 	  | Not_found ->
 	      let rel, args = relation_of_constr env (pf_concl gl) in
@@ -1412,9 +1411,11 @@ let setoid_symmetry gl =
 let setoid_transitivity c gl =
   setoid_proof gl "transitive" 
     (fun env evm car rel ->
-      apply_with_bindings
-	((get_transitive_proof env evm car rel),
-	Rawterm.ExplicitBindings [ dummy_loc, Rawterm.NamedHyp (id_of_string "y"), c ]))
+      let proof = get_transitive_proof env evm car rel in
+      match c with
+      | None -> eapply proof
+      | Some c ->
+	  apply_with_bindings (proof,Rawterm.ExplicitBindings [ dummy_loc, Rawterm.NamedHyp (id_of_string "y"), c ]))
     (transitivity_red true c)
     
 let setoid_symmetry_in id gl =
@@ -1450,7 +1451,8 @@ TACTIC EXTEND setoid_reflexivity
 END
 
 TACTIC EXTEND setoid_transitivity
-[ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity t ]
+  [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity (Some t) ]
+| [ "setoid_etransitivity" ] -> [ setoid_transitivity None ]
 END
 
 let implify id gl =
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 41ec5dc07..e436fc90f 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -798,7 +798,7 @@ let rec intern_atomic lf ist x =
   | TacReflexivity -> TacReflexivity
   | TacSymmetry idopt -> 
       TacSymmetry (clause_app (intern_hyp_location ist) idopt)
-  | TacTransitivity c -> TacTransitivity (intern_constr ist c)
+  | TacTransitivity c -> TacTransitivity (Option.map (intern_constr ist) c)
 
   (* Equality and inversion *)
   | TacRewrite (ev,l,cl,by) -> 
@@ -2338,7 +2338,7 @@ and interp_atomic ist gl = function
   (* Equivalence relations *)
   | TacReflexivity -> h_reflexivity
   | TacSymmetry c -> h_symmetry (interp_clause ist gl c)
-  | TacTransitivity c -> h_transitivity (pf_interp_constr ist gl c)
+  | TacTransitivity c -> h_transitivity (Option.map (pf_interp_constr ist gl) c)
 
   (* Equality and inversion *)
   | TacRewrite (ev,l,cl,by) -> 
@@ -2652,7 +2652,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
 
   (* Equivalence relations *)
   | TacReflexivity | TacSymmetry _ as x -> x
-  | TacTransitivity c -> TacTransitivity (subst_rawconstr subst c)
+  | TacTransitivity c -> TacTransitivity (Option.map (subst_rawconstr subst) c)
 
   (* Equality and inversion *)
   | TacRewrite (ev,l,cl,by) -> 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e96806de1..0224da6c8 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -905,16 +905,13 @@ let eapply_with_bindings (c,bl) =
 let apply c =
   apply_with_ebindings (inj_open c,NoBindings)
 
+let eapply c =
+  eapply_with_ebindings (inj_open c,NoBindings)
+
 let apply_list = function 
   | c::l -> apply_with_bindings (c,ImplicitBindings l)
   | _ -> assert false
 
-(* Resolution with no reduction on the type (used ?) *)
-
-let apply_without_reduce c gl = 
-  let clause = mk_clenv_type_of gl c in 
-  res_pf clause gl
-
 (* [apply_in hyp c] replaces
 
    hyp : forall y1, ti -> t             hyp : rho(u)
@@ -2116,9 +2113,6 @@ let mkHRefl t x =
 (*   mkApp (coq_constant "mkHEq" ["Logic";"EqdepFacts"] "eq_dep_intro", *)
 (* 	[| ty; mkApp (Lazy.force id, [|ty|]); t; x |]) *)
 
-let mkCoe a x p px y eq = 
-  mkApp (Option.get (build_coq_eq_data ()).rect, [| a; x; p; px; y; eq |])
-
 let lift_togethern n l =
   let l', _ =
     List.fold_right
@@ -3059,13 +3053,11 @@ let reflexivity_red allowred gl =
   else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl) 
   in 
     match match_with_equality_type concl with
-    | None -> None
-    | Some _ -> Some (one_constructor 1 NoBindings)
+    | None -> raise NoEquationFound
+    | Some _ -> one_constructor 1 NoBindings gl
 
-let reflexivity gl = 
-  match reflexivity_red false gl with
-  | None -> !setoid_reflexivity gl
-  | Some tac -> tac gl
+let reflexivity gl =
+  try reflexivity_red false gl with NoEquationFound -> !setoid_reflexivity gl
       
 let intros_reflexivity  = (tclTHEN intros reflexivity)
 
@@ -3079,41 +3071,35 @@ let intros_reflexivity  = (tclTHEN intros reflexivity)
 let setoid_symmetry = ref (fun _ -> assert false)
 let register_setoid_symmetry f = setoid_symmetry := f
 
+(* This is probably not very useful any longer *)
+let prove_symmetry hdcncl eq_kind =
+  let symc =
+    match eq_kind with
+    | MonomorphicLeibnizEq (c1,c2) -> mkApp(hdcncl,[|c2;c1|])
+    | PolymorphicLeibnizEq (typ,c1,c2) -> mkApp(hdcncl,[|typ;c2;c1|])
+    | HeterogenousEq (t1,c1,t2,c2) -> mkApp(hdcncl,[|t2;c2;t1;c1|]) in
+  tclTHENFIRST (cut symc)
+    (tclTHENLIST 
+      [ intro; 
+        onLastHyp simplest_case; 
+	one_constructor 1 NoBindings ])
+
 let symmetry_red allowred gl =
   (* PL: usual symmetry don't perform any reduction when searching 
      for an equality, but we may need to do some when called back from 
      inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
-  let concl = if not allowred then pf_concl gl
-  else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl) 
+  let concl =
+    if not allowred then pf_concl gl else pf_whd_betadeltaiota gl (pf_concl gl)
   in 
-    match match_with_equation concl with
-    | None -> None
-    | Some (hdcncl,args) -> Some (fun gl ->
-        let hdcncls = string_of_inductive hdcncl in
-        begin 
-	  try 
-            tclTHEN
-              (convert_concl_no_check concl DEFAULTcast)
-	      (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 
-	    in 
-	    tclTHENFIRST (cut symc)
-              (tclTHENLIST 
-		[ intro;
-		  onLastHyp simplest_case;
-		  one_constructor 1 NoBindings ])
-	      gl
-	end)
-
-let symmetry gl = 
-  match symmetry_red false gl with
-  | None -> !setoid_symmetry gl
-  | Some tac -> tac gl
+  match match_with_equation concl with
+  | Some eq_data,_,_ ->
+      tclTHEN
+        (convert_concl_no_check concl DEFAULTcast)
+      (apply eq_data.sym) gl
+  | None,eq,eq_kind -> prove_symmetry eq eq_kind gl
+
+let symmetry gl =
+  try symmetry_red false gl with NoEquationFound -> !setoid_symmetry gl
 
 let setoid_symmetry_in = ref (fun _ _ -> assert false)
 let register_setoid_symmetry_in f = setoid_symmetry_in := f
@@ -3121,18 +3107,17 @@ let register_setoid_symmetry_in f = setoid_symmetry_in := f
 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 -> !setoid_symmetry_in id gl
-    | 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
+  try 
+    let _,hdcncl,eq = match_with_equation t in
+    let symccl = match eq with
+      | MonomorphicLeibnizEq (c1,c2) -> mkApp (hdcncl, [| c2; c1 |])
+      | PolymorphicLeibnizEq (typ,c1,c2) -> mkApp (hdcncl, [| typ; c2; c1 |])
+      | HeterogenousEq (t1,c1,t2,c2) -> mkApp (hdcncl, [| t2; c2; t1; c1 |]) in
+    tclTHENS (cut (it_mkProd_or_LetIn symccl sign))
+      [ intro_replacing id;
+        tclTHENLIST [ intros; symmetry; apply (mkVar id); assumption ] ]
+      gl
+  with NoEquationFound -> !setoid_symmetry_in id gl
 
 let intros_symmetry =
   onClause
@@ -3155,47 +3140,52 @@ let intros_symmetry =
 let setoid_transitivity = ref (fun _ _ -> assert false)
 let register_setoid_transitivity f = setoid_transitivity := f
 
+(* This is probably not very useful any longer *)
+let prove_transitivity hdcncl eq_kind t gl =
+  let eq1,eq2 =
+    match eq_kind with
+    | MonomorphicLeibnizEq (c1,c2) ->
+      (mkApp (hdcncl, [| c1; t|]), mkApp (hdcncl, [| t; c2 |]))
+  | PolymorphicLeibnizEq (typ,c1,c2) ->
+      (mkApp (hdcncl, [| typ; c1; t |]), mkApp (hdcncl, [| typ; t; c2 |]))
+  | HeterogenousEq (typ1,c1,typ2,c2) ->
+      let typt = pf_type_of gl t in
+      (mkApp(hdcncl, [| typ1; c1; typt ;t |]),
+       mkApp(hdcncl, [| typt; t; typ2; c2 |])) in
+  tclTHENFIRST (cut eq2)
+    (tclTHENFIRST (cut eq1)
+      (tclTHENLIST
+	[ tclDO 2 intro;
+	  onLastHyp simplest_case;
+	  assumption ])) gl
+
 let transitivity_red allowred t gl =
   (* PL: usual transitivity don't perform any reduction when searching 
      for an equality, but we may need to do some when called back from 
      inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
-  let concl = if not allowred then pf_concl gl
-  else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl) 
-  in 
+  let concl =
+    if not allowred then pf_concl gl else pf_whd_betadeltaiota gl (pf_concl gl)
+  in
   match match_with_equation concl with
-    | None -> None
-    | Some (hdcncl,args) -> Some (fun gl ->
-        let hdcncls = string_of_inductive hdcncl in
-        begin
-	  try 
-	    apply_list [(pf_parse_const gl ("trans_"^hdcncls));t] gl 
-          with  _ -> 
-            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
-            tclTHENFIRST (cut eq2)
-	      (tclTHENFIRST (cut eq1)
-                (tclTHENLIST
-		  [ tclDO 2 intro;
-		    onLastHyp simplest_case;
-		    assumption ])) gl
-        end)
-
-let transitivity t gl =
-  match transitivity_red false t gl with
-  | None -> !setoid_transitivity t gl
-  | Some tac -> tac gl
-      
-let intros_transitivity  n  = tclTHEN intros (transitivity n)
+  | Some eq_data,_,_ ->
+      tclTHEN
+        (convert_concl_no_check concl DEFAULTcast)
+        (match t with
+	 | None -> eapply eq_data.trans
+	 | Some t -> apply_list [eq_data.trans;t]) gl
+  | None,eq,eq_kind ->
+      match t with
+      | None -> error "etransitivity not supported for this relation."
+      | Some t -> prove_transitivity eq eq_kind t gl
+
+let transitivity_gen t gl =
+  try transitivity_red false t gl
+  with NoEquationFound -> !setoid_transitivity t gl
+
+let etransitivity = transitivity_gen None
+let transitivity t = transitivity_gen (Some t)
+
+let intros_transitivity  n  = tclTHEN intros (transitivity_gen n)
 
 (* tactical to save as name a subproof such that the generalisation of 
    the current goal, abstracted with respect to the local signature, 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 355380a74..40740c3a8 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -176,10 +176,9 @@ val apply_type : constr -> constr list -> tactic
 val apply_term : constr -> constr list -> tactic
 val bring_hyps : named_context -> tactic
 
-val apply                 : constr      -> tactic
-val apply_without_reduce  : constr      -> tactic
-val apply_list            : constr list -> tactic
-  
+val apply                 : constr -> tactic
+val eapply                : constr -> tactic
+
 val apply_with_ebindings_gen : 
   advanced_flag -> evars_flag -> open_constr with_ebindings list -> tactic
 
@@ -271,8 +270,8 @@ val simple_induct : quantified_hypothesis -> tactic
 
 val new_induct : evars_flag -> constr with_ebindings induction_arg list -> 
   constr with_ebindings option -> 
-  intro_pattern_expr located option * intro_pattern_expr located option ->
-  clause option -> tactic
+    intro_pattern_expr located option * intro_pattern_expr located option ->
+      clause option -> tactic
 
 (*s Case analysis tactics. *)
 
@@ -282,16 +281,16 @@ val simplest_case         : constr -> tactic
 val simple_destruct          : quantified_hypothesis -> tactic
 val new_destruct : evars_flag -> constr with_ebindings induction_arg list -> 
   constr with_ebindings option -> 
-  intro_pattern_expr located option * intro_pattern_expr located option ->
-  clause option -> tactic
+    intro_pattern_expr located option * intro_pattern_expr located option ->
+      clause option -> tactic
 
 (*s Generic case analysis / induction tactics. *)
 
 val induction_destruct : evars_flag -> rec_flag -> 
   (constr with_ebindings induction_arg list *
-   constr with_ebindings option *
-   (intro_pattern_expr located option * intro_pattern_expr located option) *
-   clause option) list ->
+  constr with_ebindings option *
+  (intro_pattern_expr located option * intro_pattern_expr located option) *
+  clause option) list ->
     tactic
 
 (*s Eliminations giving the type instead of the proof. *)
@@ -312,7 +311,7 @@ val dorE : bool -> clause ->tactic
 (*s Introduction tactics. *)
 
 val constructor_tac      : evars_flag -> int option -> int -> 
-                           open_constr bindings  -> tactic
+  open_constr bindings  -> tactic
 val any_constructor      : evars_flag -> tactic option -> tactic
 val one_constructor      : int -> open_constr bindings  -> tactic
 
@@ -331,21 +330,22 @@ val simplest_split       : tactic
 (*s Logical connective tactics. *)
 
 val register_setoid_reflexivity : tactic -> unit
-val reflexivity_red             : bool -> goal sigma -> tactic option
+val reflexivity_red             : bool -> tactic
 val reflexivity                 : tactic
 val intros_reflexivity          : tactic
 
 val register_setoid_symmetry : tactic -> unit
-val symmetry_red                : bool -> goal sigma -> tactic option
+val symmetry_red                : bool -> tactic
 val symmetry                    : tactic
 val register_setoid_symmetry_in : (identifier -> tactic) -> unit
 val symmetry_in                 : identifier -> tactic
 val intros_symmetry             : clause -> tactic
 
-val register_setoid_transitivity : (constr -> tactic) -> unit
-val transitivity_red            : bool -> constr -> goal sigma -> tactic option
+val register_setoid_transitivity : (constr option -> tactic) -> unit
+val transitivity_red            : bool -> constr option -> tactic
 val transitivity                : constr -> tactic
-val intros_transitivity         : constr -> tactic
+val etransitivity               : tactic
+val intros_transitivity         : constr option -> tactic
 
 val cut                         : constr -> tactic
 val cut_intro                   : constr -> tactic
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index 1211d3327..7d9e11296 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -28,44 +28,61 @@ Set Elimination Schemes.
 
 Hint Resolve JMeq_refl.
 
-Lemma sym_JMeq : forall (A B:Type) (x:A) (y:B), JMeq x y -> JMeq y x.
+Lemma JMeq_sym : forall (A B:Type) (x:A) (y:B), JMeq x y -> JMeq y x.
+Proof.
 destruct 1; trivial.
 Qed.
 
-Hint Immediate sym_JMeq.
+Hint Immediate JMeq_sym.
 
-Lemma trans_JMeq :
+Lemma JMeq_trans :
  forall (A B C:Type) (x:A) (y:B) (z:C), JMeq x y -> JMeq y z -> JMeq x z.
-destruct 1; trivial.
+Proof.
+destruct 2; trivial.
 Qed.
 
 Axiom JMeq_eq : forall (A:Type) (x y:A), JMeq x y -> x = y.
 
-Lemma JMeq_ind : forall (A:Type) (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.
+Lemma JMeq_ind : forall (A:Type) (x:A) (P:A -> Prop), 
+  P x -> forall y, JMeq x y -> P y.
+Proof.
+intros A x P H y H'; case JMeq_eq with (1 := H'); trivial.
 Qed.
 
-Lemma JMeq_rec : forall (A:Type) (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.
+Lemma JMeq_rec : forall (A:Type) (x:A) (P:A -> Set), 
+  P x -> forall y, JMeq x y -> P y.
+Proof.
+intros A x P H y H'; case JMeq_eq with (1 := H'); trivial.
 Qed.
 
-Lemma JMeq_rect : forall (A:Type) (x y:A) (P:A->Type), P x -> JMeq x y -> P y.
-intros A x y P H H'; case JMeq_eq with (1 := H'); trivial.
+Lemma JMeq_rect : forall (A:Type) (x:A) (P:A->Type),
+  P x -> forall y, JMeq x y -> P y.
+Proof.
+intros A x P H y H'; case JMeq_eq with (1 := H'); trivial.
 Qed.
 
-Lemma JMeq_ind_r :
- forall (A:Type) (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.
+Lemma JMeq_ind_r : forall (A:Type) (x:A) (P:A -> Prop), 
+   P x -> forall y, JMeq y x -> P y.
+Proof.
+intros A x P H y H'; case JMeq_eq with (1 := JMeq_sym H'); trivial.
 Qed.
 
-Lemma JMeq_rec_r :
- forall (A:Type) (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.
+Lemma JMeq_rec_r : forall (A:Type) (x:A) (P:A -> Set),
+   P x -> forall y, JMeq y x -> P y.
+Proof.
+intros A x P H y H'; case JMeq_eq with (1 := JMeq_sym H'); trivial.
+Qed.
+
+Lemma JMeq_rect_r : forall (A:Type) (x:A) (P:A -> Type),
+   P x -> forall y, JMeq y x -> P y.
+Proof.
+intros A x P H y H'; case JMeq_eq with (1 := JMeq_sym H'); trivial.
 Qed.
 
-Lemma JMeq_rect_r :
- forall (A:Type) (x y:A) (P:A -> Type), P y -> JMeq x y -> P x.
-intros A x y P H H'; case JMeq_eq with (1 := sym_JMeq H'); trivial.
+Lemma JMeq_congr :
+ forall (A B:Type) (f:A->B) (x y:A), JMeq x y -> JMeq (f x) (f y).
+Proof.
+intros A B f x y H; case JMeq_eq with (1 := H); trivial.
 Qed.
 
 (** [JMeq] is equivalent to [eq_dep Type (fun X => X)] *)
@@ -107,3 +124,7 @@ intro H.
 assert (true=false) by (destruct H; reflexivity).
 discriminate.
 Qed.
+
+(* Compatibility *)
+Notation sym_JMeq := JMeq_sym (only parsing).
+Notation trans_JMeq := JMeq_trans (only parsing).
diff --git a/toplevel/coqcompat.ml b/toplevel/coqcompat.ml
index 8bf1e9bd0..59dca330c 100644
--- a/toplevel/coqcompat.ml
+++ b/toplevel/coqcompat.ml
@@ -24,10 +24,10 @@ let set_compat_options = function
       set_bool_option_value ["Intuition";"Iff";"Unfolding"] true
 
   | "8.1" ->
-      warning "Compatibility with versions 8.1 not supported."
+      warning "Compatibility with version 8.1 not supported."
 
   | "8.0" ->
-      warning "Compatibility with versions 8.0 not supported."
+      warning "Compatibility with version 8.0 not supported."
 
   | s ->
       error ("Unknown compatibility version \""^s^"\".")