From 7a58ae18892816cf494aa834e706a6b10200b1c0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 19 Sep 2017 00:25:21 +0200
Subject: [PATCH] =?UTF-8?q?Rename=20fix.v=20=E2=86=92=20fixpoint.v=20becau?=
=?UTF-8?q?se=20fix=20is=20a=20reserved=20keyword.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
That caused some problems, e.g.:
From iris.base_logic Require Export fix.
Gave:
Syntax error: [constr:global] expected after
[export_token] (in [vernac:gallina_ext]).
---
_CoqProject | 2 +-
theories/base_logic/{fix.v => fixpoint.v} | 0
2 files changed, 1 insertion(+), 1 deletion(-)
rename theories/base_logic/{fix.v => fixpoint.v} (100%)
diff --git a/_CoqProject b/_CoqProject
index 76621c1e8..6fac0e791 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -34,7 +34,7 @@ theories/base_logic/hlist.v
theories/base_logic/soundness.v
theories/base_logic/double_negation.v
theories/base_logic/deprecated.v
-theories/base_logic/fix.v
+theories/base_logic/fixpoint.v
theories/base_logic/lib/iprop.v
theories/base_logic/lib/own.v
theories/base_logic/lib/saved_prop.v
diff --git a/theories/base_logic/fix.v b/theories/base_logic/fixpoint.v
similarity index 100%
rename from theories/base_logic/fix.v
rename to theories/base_logic/fixpoint.v
--
GitLab