From 0b4d25e770fdb542fd47efdb248361672b3dbfb5 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Mon, 1 May 2023 21:35:26 +0200 Subject: [PATCH] Use `#[projections(primitive=yes)]` pragma. --- stdpp/base.v | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/stdpp/base.v b/stdpp/base.v index 38684100..45e5a5f8 100644 --- a/stdpp/base.v +++ b/stdpp/base.v @@ -52,10 +52,8 @@ Add Search Blacklist "_obligation_". Add Search Blacklist "_unseal". (** * Sealing off definitions *) -Section seal. - Local Set Primitive Projections. - Record seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }. -End seal. +#[projections(primitive=yes)] +Record seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }. Global Arguments unseal {_ _} _ : assert. Global Arguments seal_eq {_ _} _ : assert. -- GitLab