From b938e033b427e9839ed90c37e5ba4bd18a529870 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 4 Mar 2019 07:25:27 +0100
Subject: [PATCH] Make `fresh` stuff `simpl never`.

This fixes an issue in orc11.
---
 theories/base.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/base.v b/theories/base.v
index ab0ca483..464ba6db 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -1226,12 +1226,14 @@ aforementioned [fresh] function on finite sets that respects set equality. *)
 Class Fresh A C := fresh: C → A.
 Hint Mode Fresh - ! : typeclass_instances.
 Instance: Params (@fresh) 3 := {}.
+Arguments fresh : simpl never.
 
 Class Infinite A := {
   infinite_fresh :> Fresh A (list A);
   infinite_is_fresh (xs : list A) : fresh xs ∉ xs;
   infinite_fresh_Permutation :> Proper (@Permutation A ==> (=)) fresh;
 }.
+Arguments infinite_fresh : simpl never.
 
 (** * Miscellaneous *)
 Class Half A := half: A → A.
-- 
GitLab