Commit cf692104 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

remove Warnings in Field, add Field files to the `make all` target

parent 21e88b2c
Set Warnings "-notation-overridden,-parsing".
From mathcomp Require Import ssreflect ssrbool eqtype seq ssrfun ssrnat ssralg ssrint.
From Tweetnacl Require Import Libs.Export.
From Tweetnacl Require Import ListsOp.Export.
default_target: .loadpath Libs ListsOp Mid Low
default_target: .loadpath Libs ListsOp Mid Low
all: default_target High
all: default_target Field High
#Note3: for SSReflect, one solution is to install MathComp 1.6
# somewhere add this line to a CONFIGURE file
......@@ -12,7 +12,7 @@ SHOW := $(if $(VERBOSE),@true "",@echo "")
HIDE := $(if $(VERBOSE),,@)
DIRS= Libs ListsOp Mid Low High
DIRS= Libs ListsOp Mid Low High Field
INCLUDE= $(foreach a,$(DIRS),$(if $(wildcard $(a)), -Q $(a) $(a)))
COQFLAGS=$(foreach d, $(DIRS), $(if $(wildcard $(d)), -Q $(d) $(d))) $(EXTFLAGS)
......@@ -39,6 +39,7 @@ LISTSOP_FILES = $(wildcard ListsOp/*.v)
MID_FILES = $(wildcard Mid/*.v)
LOW_FILES = $(wildcard Low/*.v)
HIGH_FILES = $(wildcard High/*.v)
FIELD_FILES = $(wildcard Field/*.v)
......@@ -87,6 +88,7 @@ ListsOp: .loadpath $(LISTSOP_FILES:%.v=%.vo)
Mid: .loadpath $(MID_FILES:%.v=%.vo)
Low: .loadpath $(LOW_FILES:%.v=%.vo)
High: .loadpath $(HIGH_FILES:%.v=%.vo)
Field: .loadpath $(FIELD_FILES:%.v=%.vo)
_CoqProject: Makefile
$(SHOW)Generate _CoqProject
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment