Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Benoit Viguier
coq-verif-tweetnacl
Commits
d443401f
Commit
d443401f
authored
May 09, 2018
by
Benoit Viguier
Browse files
allow coq.dev
parent
310471bd
Changes
2
Hide whitespace changes
Inline
Side-by-side
Libs/Lists_extended.v
View file @
d443401f
Require
Import
stdpp
.
prelude
.
From
Tweetnacl
Require
Import
Libs
.
LibTactics
.
From
Tweetnacl
Require
Import
Libs
.
LibTactics_SF
.
Require
Import
mathcomp
.
ssreflect
.
ssreflect
.
Require
Import
stdpp
.
list
.
Section
nth_f
.
Context
{
I
}
{
O
}
(
f
:
I
->
O
)
(
v
:
I
).
...
...
Makefile
View file @
d443401f
...
...
@@ -28,7 +28,7 @@ COQTOP=$(COQBIN)coqtop
COQDEP
=
$(COQBIN)
coqdep
$(DEPFLAGS)
COQDOC
=
$(COQBIN)
coqdoc
-d
doc
-g
-utf8
$(DEPFLAGS)
COQVERSION
=
8.7.0 or-else 8.7.1 or-else 8.7.2 or-else 8.8.0
COQVERSION
=
8.7.0 or-else 8.7.1 or-else 8.7.2 or-else 8.8.0
or-else 8.8+alpha
COQV
=
$(
shell
$(COQC)
-v
)
ifeq
("$(filter $(COQVERSION),$(COQV))","")
$(error FAILURE
:
You need Coq $(COQVERSION) but you have this version: $(COQV))
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment