diff options
| author | puech | 2011-07-29 14:29:23 +0000 |
|---|---|---|
| committer | puech | 2011-07-29 14:29:23 +0000 |
| commit | 0cfb71569ad334822e9efcd82cd5215569301b27 (patch) | |
| tree | bd12d5af193a824dc1161705b6e7fc1ecc46bcb6 /plugins | |
| parent | 31d034155b5abe0bfc0cfd69b88603c954b6229e (diff) | |
replaced some generic = on constr by eq_constr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14364 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/setoid_ring/newring.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 0df4bed0aa..4a70ffd8d2 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -891,7 +891,7 @@ let dest_field env sigma th_spec = let th_typ = Retyping.get_type_of env sigma th_spec in match kind_of_term th_typ with | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|]) - when f = Lazy.force afield_theory -> + when eq_constr f (Lazy.force afield_theory) -> let rth = lapp af_ar [|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) @@ -902,7 +902,7 @@ let dest_field env sigma th_spec = [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in (Some false,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth) | App(f,[|r;zero;one;add;mul;div;inv;req|]) - when f = Lazy.force sfield_theory -> + when eq_constr f (Lazy.force sfield_theory) -> let rth = lapp sf_sr [|r;zero;one;add;mul;div;inv;req;th_spec|] in (Some true,r,zero,one,add,mul,None,None,div,inv,req,rth) |