diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-08-03 20:50:11 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-08-03 20:50:11 +0000 |
| commit | f9f35dc36f5249a2de18005ab59ae934e0fa7075 (patch) | |
| tree | 4d3dd839db319df1945c8fef474284e6f4e5f3e3 /plugins/field | |
| parent | 25dde2366a4db47e5da13b2bbe4d03a31235706f (diff) | |
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
Diffstat (limited to 'plugins/field')
| -rw-r--r-- | plugins/field/field.ml4 | 10 |
1 files changed, 6 insertions, 4 deletions
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 |