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

9 files changed, 227 insertions, 178 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index ce0677caef..101e7ef8c2 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 b85491c57d..65a56100bf 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 5aafb91a0d..f5b2dbb552 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 7086e44219..0b81a492ac 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 3418dd208e..5be8b20264 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 52f10d46c6..43ae99203d 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 41ec5dc07b..e436fc90f5 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 e96806de1c..0224da6c87 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 355380a74c..40740c3a82 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