Version update coq 8.5pl2 => 8.7.0

README.md

@@ -7,12 +7,12 @@ verified validators.
 Requirements
 ------------
 
-*   OCaml 4.03.0
-    *   ocamlfind 1.6.2
-    *   ocamlbuild 0.9.2
-    *   ocamlgraph 1.8.7
+*   OCaml 4.04.2
+    *   ocamlfind 1.7.3
+    *   ocamlbuild 0.11.0
+    *   ocamlgraph 1.8.8
     *   cil 1.7.3
-*   Coq 8.5pl2
+*   Coq 8.7.0
 
 How to make (example: the interval analyzer)
 --------------------------------------------

spec/.gitignore

@@ -1 +1,2 @@
 Makefile.coq
+Makefile.coq.conf

spec/Basic/.dir-locals.el

@@ -1,2 +1,2 @@
 ((coq-mode . ((coq-prog-args .
-  ("-emacs-U" "-R" "." "Basic")))))
+  ("-R" "." "Basic")))))

spec/Basic/DFMapAVL.v

@@ -14,6 +14,7 @@ Set Implicit Arguments.
 Require Import OrderedType FMapAVL.
 Require FMapFacts.
 Require Import VocabA.
+Require Import FunInd.
 
 Local Open Scope bool.
 

spec/Basic/DNList.v

@@ -135,20 +135,21 @@ Fixpoint eq_dec' s (x y : t) : {eq' s x y} + {~ eq' s x y}.
 refine
   match s with
     | O => left (eq_zero x y)
-    | S s' =>
-      match x, y with
-        | nil, nil => left _
-        | cons hd1 tl1, cons hd2 tl2 =>
-          match A.eq_dec hd1 hd2 with
-            | left _ =>
-              match eq_dec' s' tl1 tl2 with
-                | left _ => left _
-                | right _ => right _
-              end
-            | right _ => right _
-          end
-        | _, _ => right _
+    | S s' => _
+  end;
+refine
+  match x, y with
+  | nil, nil => left _
+  | cons hd1 tl1, cons hd2 tl2 =>
+    match A.eq_dec hd1 hd2 with
+    | left _ =>
+      match eq_dec' s' tl1 tl2 with
+      | left _ => left _
+      | right _ => right _
       end
+    | right _ => right _
+    end
+  | _, _ => right _
   end; try (by inversion 1).
 - apply eq_nil.
 - apply eq_cons; auto.

spec/Basic/TStr.v

@@ -11,6 +11,7 @@ Set Implicit Arguments.
 will be extracted to string type of OCaml. *)
 
 Require Import OrderedType OrderedTypeEx.
+Require Extraction.
 
 Axiom string_t : Type.
 Extract Constant string_t => "string".

spec/ItvInput/.dir-locals.el

@@ -1,2 +1,2 @@
 ((coq-mode . ((coq-prog-args .
-  ("-emacs-U" "-R" "../Basic" "Basic" "-R" "." "ItvInput")))))
+  ("-R" "../Basic" "Basic" "-R" "." "ItvInput")))))

spec/ItvInputProof/.dir-locals.el

@@ -1,2 +1,2 @@
 ((coq-mode . ((coq-prog-args .
-  ("-emacs-U" "-R" "../Basic" "Basic" "-R" "../ItvInput" "ItvInput" "-R" "../Gen" "Gen" "-R" "../Proof" "Proof" "-R" "." "ItvInputProof")))))
+  ("-R" "../Basic" "Basic" "-R" "../ItvInput" "ItvInput" "-R" "../Gen" "Gen" "-R" "../Proof" "Proof" "-R" "." "ItvInputProof")))))

spec/Proof/.dir-locals.el

@@ -1,2 +1,2 @@
 ((coq-mode . ((coq-prog-args .
-  ("-emacs-U" "-R" "../Basic" "Basic" "-R" "." "Proof")))))
+  ("-R" "../Basic" "Basic" "-R" "." "Proof")))))

spec/TntInput/.dir-locals.el

@@ -1,2 +1,2 @@
 ((coq-mode . ((coq-prog-args .
-  ("-emacs-U" "-R" "../Basic" "Basic" "-R" "." "TntInput")))))
+  ("-R" "../Basic" "Basic" "-R" "." "TntInput")))))

spec/TntInputProof/.dir-locals.el

@@ -1,2 +1,2 @@
 ((coq-mode . ((coq-prog-args .
-  ("-emacs-U" "-R" "../Basic" "Basic" "-R" "../TntInput" "TntInput" "-R" "../Gen" "Gen" "-R" "../Proof" "Proof" "-R" "." "TntInputProof")))))
+  ("-R" "../Basic" "Basic" "-R" "../TntInput" "TntInput" "-R" "../Gen" "Gen" "-R" "../Proof" "Proof" "-R" "." "TntInputProof")))))