Skip to content

Commit 111be55

Browse files
committed
Remove Stdlib dependency
1 parent 39154ba commit 111be55

File tree

2 files changed

+9
-1
lines changed

2 files changed

+9
-1
lines changed

Makefile.coq.local

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
pre-all::
2+
if command -v coqc > /dev/null && (coqc --version | grep -q '8.18\|8.19\|8.20') ; then \
3+
for f in $(shell grep "From Corelib" $$(find . -name "*.v") | cut -d: -f1) ; do \
4+
sed -i.bak $${f} -e 's/From Corelib/From Coq/' ; \
5+
sed -i.bak $${f} -e 's/PosDef/PArith/' ; \
6+
$(RM) $${f}.bak ; \
7+
done ; \
8+
fi

theories/PFsection1.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
22
(* Distributed under the terms of CeCILL-B. *)
3-
From Coq Require Import RelationClasses.
3+
From Corelib Require Import RelationClasses.
44
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
55
From mathcomp Require Import div choice fintype tuple finfun bigop prime finset.
66
From mathcomp Require Import order.

0 commit comments

Comments
 (0)