diff options
| author | puech | 2011-07-29 14:28:34 +0000 |
|---|---|---|
| committer | puech | 2011-07-29 14:28:34 +0000 |
| commit | a2881fa16dccf274a82bbec08ee7b1224df0d1da (patch) | |
| tree | b74f0bf5f35c9494a27b886e1cf096326a7e4e7b | |
| parent | c9624662706ea91a139241ce9953860f754302eb (diff) | |
Newring: replaced some generic = on constr by eq_constr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14356 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | plugins/setoid_ring/newring.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 7f1bf81d19..0df4bed0aa 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -590,10 +590,10 @@ let dest_morph env sigma m_spec = match kind_of_term m_typ with App(f,[|r;zero;one;add;mul;sub;opp;req; c;czero;cone;cadd;cmul;csub;copp;ceqb;phi|]) - when f = Lazy.force coq_ring_morph -> + when eq_constr f (Lazy.force coq_ring_morph) -> (c,czero,cone,cadd,cmul,Some csub,Some copp,ceqb,phi) | App(f,[|r;zero;one;add;mul;req;c;czero;cone;cadd;cmul;ceqb;phi|]) - when f = Lazy.force coq_semi_morph -> + when eq_constr f (Lazy.force coq_semi_morph) -> (c,czero,cone,cadd,cmul,None,None,ceqb,phi) | _ -> error "bad morphism structure" @@ -896,7 +896,7 @@ let dest_field env sigma th_spec = [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in (None,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth) | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|]) - when f = Lazy.force field_theory -> + when eq_constr f (Lazy.force field_theory) -> let rth = lapp f_r [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in |