diff options
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. |