From f9f35dc36f5249a2de18005ab59ae934e0fa7075 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 3 Aug 2009 20:50:11 +0000
Subject: 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
---
 plugins/field/field.ml4 | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'plugins/field')

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
-- 
cgit v1.2.3