diff options
| author | Enrico Tassi | 2019-04-30 15:24:14 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-04-30 15:24:14 +0200 |
| commit | 4ac61e9dbf227356edfe33b683a6638776e52c5d (patch) | |
| tree | bf1ed55f32b65e6c6cf98aa0af8e434578c62175 /test-suite/prerequisite | |
| parent | 823bde2eaffbacdb7a3a08c9d7274cd84dc5bef5 (diff) | |
| parent | 7875955f513f55c1fcef90becdaaa572baa3e5ae (diff) | |
Merge PR #9995: fix `simpl_rel` and notations, `{pred T}` alias, `nonPropType` interface
Ack-by: SkySkimmer
Reviewed-by: gares
Ack-by: ggonthier
Diffstat (limited to 'test-suite/prerequisite')
| -rw-r--r-- | test-suite/prerequisite/ssr_mini_mathcomp.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/prerequisite/ssr_mini_mathcomp.v b/test-suite/prerequisite/ssr_mini_mathcomp.v index ca360f65a7..6fc630056c 100644 --- a/test-suite/prerequisite/ssr_mini_mathcomp.v +++ b/test-suite/prerequisite/ssr_mini_mathcomp.v @@ -634,9 +634,9 @@ Fixpoint mem_seq (s : seq T) := Definition eqseq_class := seq T. Identity Coercion seq_of_eqseq : eqseq_class >-> seq. -Coercion pred_of_eq_seq (s : eqseq_class) : pred_class := [eta mem_seq s]. +Coercion pred_of_eq_seq (s : eqseq_class) : {pred T} := [eta mem_seq s]. -Canonical seq_predType := @mkPredType T (seq T) pred_of_eq_seq. +Canonical seq_predType := @PredType T (seq T) pred_of_eq_seq. Fixpoint uniq s := if s is x :: s' then (x \notin s') && uniq s' else true. |