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

4 files changed, 21 insertions, 15 deletions

diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4
index 93de6118b6..c9b993690f 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 445b193f81..9e649a5a2f 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 bff8cae260..9629fa923c 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 adcf51fe85..6dcc1e8725 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