From 8ff30e0fedba9d670e45cd91b777241c4b68eeb4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 13 Oct 2017 10:42:47 +0200
Subject: [PATCH] move Arguments out of section
---
theories/base.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/base.v b/theories/base.v
index 48a5fd0f..f0964e3c 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -21,9 +21,9 @@ Add Search Blacklist "_obligation_".
Section seal.
Local Set Primitive Projections.
Record seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }.
- Arguments unseal {_ _} _ : assert.
- Arguments seal_eq {_ _} _ : assert.
End seal.
+Arguments unseal {_ _} _ : assert.
+Arguments seal_eq {_ _} _ : assert.
(** Typeclass opaque definitions *)
(* The constant [tc_opaque] is used to make definitions opaque for just type
--
GitLab