From fe5a098d8f8829cb0b7619448052807c13c85155 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 8 Feb 2016 16:31:10 +0100
Subject: [PATCH] Coq syntax nit
---
program_logic/namespace.v | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
diff --git a/program_logic/namespace.v b/program_logic/namespace.v
index 7cab6f273..76e8a34c0 100644
--- a/program_logic/namespace.v
+++ b/program_logic/namespace.v
@@ -5,8 +5,7 @@ Definition namespace := list positive.
Definition nnil : namespace := nil.
Definition ndot `{Countable A} (N : namespace) (x : A) : namespace :=
encode x :: N.
-Definition nclose (N : namespace) : coPset := coPset_suffixes (encode N).
-Coercion nclose : namespace >-> coPset.
+Coercion nclose (N : namespace) : coPset := coPset_suffixes (encode N).
Instance ndot_injective `{Countable A} : Injective2 (=) (=) (=) (@ndot A _ _).
Proof. by intros N1 x1 N2 x2 ?; simplify_equality. Qed.
--
GitLab