migration to Coq 8.7

Author: ilyasergey

.gitignore

@@ -73,12 +73,13 @@ cv/*.out
 # -----------------------------------------------------------------------------
 
 \#*\#
-*.vo 
+*.vo
 *.v.d
 *.glob
 .coq-native
 Makefile.coq
 extraction/**/*.mli
 extraction/**/*.ml
 _build
-*.d.byte
+*.d.byte
+Makefile.coq.conf

README.md

@@ -15,9 +15,9 @@ the GitHub repository; the following dependencies are necessary.
 
 ### Requirements
 
-* Coq 8.6 (available from https://coq.inria.fr/download)
+* Coq 8.7 (available from https://coq.inria.fr/download)
 * Mathematical Components 1.6.1 (http://math-comp.github.io/math-comp/)
-* OCaml 4.02.3 or later (to compile and run the extracted applications)
+* OCaml 4.05.0 or later (to compile and run the extracted applications)
 
 If Coq is not installed such that its binaries like `coqc` and
 `coq_makefile` are in the `PATH`, then the `COQBIN` environment variable

_CoqProject

@@ -1,3 +1,6 @@
+-Q . DiSeL
+-arg "-w -notation-overridden,-local-declaration,-redundant-canonical-projection,-projection-no-head-constant"
+
 -R . DiSeL
 Heaps/coding.v
 Heaps/domain.v
@@ -28,7 +31,7 @@ Core/Process.v
 Core/Always.v
 Core/HoareTriples.v
 Core/InferenceRules.v
-Core/While.v 
+Core/While.v
 Core/DiSeLExtraction.v
 Examples/SeqLib.v
 Examples/Greeter/Greeter.v