diff options
| author | Georges Gonthier | 2019-04-28 20:37:17 +0200 |
|---|---|---|
| committer | Georges Gonthier | 2019-04-29 00:26:36 +0200 |
| commit | 6be8fd5c67949a59bde7083e81401263986e7a4e (patch) | |
| tree | 71a6e45e4948db3a459906982a5b2b982470108c /mathcomp/algebra/rat.v | |
| parent | 8e27a1dd704c8f7a34de29d65337eb67254a1741 (diff) | |
Generalise use of `{pred T}` from coq/coq#9995
Use `{pred T}` systematically for generic _collective_ boolean
predicate.
Use `PredType` to construct `predType` instances.
Instrument core `ssreflect` files to replicate these and other new
features introduces by coq/coq#9555 (`nonPropType` interface,
`simpl_rel` that simplifies with `inE`).
Diffstat (limited to 'mathcomp/algebra/rat.v')
| -rw-r--r-- | mathcomp/algebra/rat.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v index 8654fd1..228a824 100644 --- a/mathcomp/algebra/rat.v +++ b/mathcomp/algebra/rat.v @@ -689,7 +689,8 @@ Proof. by rewrite /ratr numq_int denq_int divr1. Qed. Lemma ratr_nat n : ratr n%:R = n%:R. Proof. exact: (ratr_int n). Qed. -Lemma rpred_rat S (ringS : @divringPred R S) (kS : keyed_pred ringS) a : +Lemma rpred_rat (S : {pred R}) (ringS : divringPred S) (kS : keyed_pred ringS) + a : ratr a \in kS. Proof. by rewrite rpred_div ?rpred_int. Qed. |