diff options
| author | herbelin | 2009-08-03 20:50:11 +0000 |
|---|---|---|
| committer | herbelin | 2009-08-03 20:50:11 +0000 |
| commit | f9f35dc36f5249a2de18005ab59ae934e0fa7075 (patch) | |
| tree | 4d3dd839db319df1945c8fef474284e6f4e5f3e3 /plugins/ring | |
| 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/ring')
| -rw-r--r-- | plugins/ring/ring.ml | 20 |
1 files changed, 11 insertions, 9 deletions
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 |