diff options
| -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 38c65cdd0..e63dbba42 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -574,13 +574,13 @@ let dest_ring 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;req|]) - when f = Lazy.force coq_almost_ring_theory -> + when eq_constr f (Lazy.force coq_almost_ring_theory) -> (None,r,zero,one,add,mul,Some sub,Some opp,req) | App(f,[|r;zero;one;add;mul;req|]) - when f = Lazy.force coq_semi_ring_theory -> + when eq_constr f (Lazy.force coq_semi_ring_theory) -> (Some true,r,zero,one,add,mul,None,None,req) | App(f,[|r;zero;one;add;mul;sub;opp;req|]) - when f = Lazy.force coq_ring_theory -> + when eq_constr f (Lazy.force coq_ring_theory) -> (Some false,r,zero,one,add,mul,Some sub,Some opp,req) | _ -> error "bad ring structure" |