diff options
Diffstat (limited to 'plugins/micromega/RingMicromega.v')
| -rw-r--r-- | plugins/micromega/RingMicromega.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v index 68add5b3d..fb16c55c2 100644 --- a/plugins/micromega/RingMicromega.v +++ b/plugins/micromega/RingMicromega.v @@ -57,7 +57,7 @@ Variables ceqb cleb : C -> C -> bool. Variable phi : C -> R. (* Power coefficients *) -Variable E : Set. (* the type of exponents *) +Variable E : Type. (* the type of exponents *) Variable pow_phi : N -> E. Variable rpow : R -> E -> R. @@ -78,9 +78,9 @@ Record SORaddon := mk_SOR_addon { Variable addon : SORaddon. Add Relation R req - reflexivity proved by sor.(SORsetoid).(@Equivalence_Reflexive _ _ ) - symmetry proved by sor.(SORsetoid).(@Equivalence_Symmetric _ _ ) - transitivity proved by sor.(SORsetoid).(@Equivalence_Transitive _ _ ) + reflexivity proved by sor.(SORsetoid).(@Equivalence_Reflexive _ _) + symmetry proved by sor.(SORsetoid).(@Equivalence_Symmetric _ _) + transitivity proved by sor.(SORsetoid).(@Equivalence_Transitive _ _) as micomega_sor_setoid. Add Morphism rplus with signature req ==> req ==> req as rplus_morph. @@ -414,7 +414,7 @@ Proof. simpl ; intros. destruct (nth_in_or_default n l (Pc cO, Equal)). (* index is in bounds *) - apply H ; congruence. + apply H. congruence. (* index is out-of-bounds *) inversion H0. rewrite e. simpl. |