aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/ssr/ssrbool.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v
index f6b192c226..475859fcc2 100644
--- a/plugins/ssr/ssrbool.v
+++ b/plugins/ssr/ssrbool.v
@@ -1184,7 +1184,6 @@ Notation xpreim := (fun f (p : pred _) x => p (f x)).
(** The packed class interface for pred-like types. **)
-#[universes(template)]
Structure predType T :=
PredType {pred_sort :> Type; topred : pred_sort -> pred T}.