From c7f299a5fc46e85e82043db438b5e9f17a101e79 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 29 Jan 2021 18:45:04 +0100
Subject: [PATCH] Do not mangle names in test file.

---
 tests/eunify.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/tests/eunify.v b/tests/eunify.v
index c12cc618..96eb3e66 100644
--- a/tests/eunify.v
+++ b/tests/eunify.v
@@ -1,4 +1,5 @@
 From stdpp Require Import tactics strings.
+Unset Mangle Names.
 
 Check "eunify_test".
 Lemma eunify_test : ∀ x y, 0 < S x + y.
-- 
GitLab