diff options
Diffstat (limited to 'plugins/setoid_ring/Field_theory.v')
| -rw-r--r-- | plugins/setoid_ring/Field_theory.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index 205bef6d5..9617d4091 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -439,11 +439,11 @@ Fixpoint PExpr_eq (e1 e2 : PExpr C) {struct e1} : bool := | _, _ => false end. -Add Morphism (pow_pos rmul) : pow_morph. +Add Morphism (pow_pos rmul) with signature req ==> eq ==> req as pow_morph. intros x y H p;induction p as [p IH| p IH|];simpl;auto;ring[IH]. Qed. -Add Morphism (pow_N rI rmul) with signature req ==> (@eq N) ==> req as pow_N_morph. +Add Morphism (pow_N rI rmul) with signature req ==> eq ==> req as pow_N_morph. intros x y H [|p];simpl;auto. apply pow_morph;trivial. Qed. (* |