Merge pull request #10 from clarus/upgade-to-coq-8.10

Add compatibility with Coq 8.10

Author: clarus

.travis.yml

@@ -13,8 +13,8 @@ env:
   - COQ_IMAGE="coqorg/coq:8.6"  SHOULD_SUPPORT="false"
   - COQ_IMAGE="coqorg/coq:8.7"  SHOULD_SUPPORT="true"
   - COQ_IMAGE="coqorg/coq:8.8"  SHOULD_SUPPORT="true"
-  - COQ_IMAGE="coqorg/coq:8.9"  SHOULD_SUPPORT="false"
-  - COQ_IMAGE="coqorg/coq:8.10" SHOULD_SUPPORT="false"
+  - COQ_IMAGE="coqorg/coq:8.9"  SHOULD_SUPPORT="true"
+  - COQ_IMAGE="coqorg/coq:8.10" SHOULD_SUPPORT="true"
 
 install: |
   # Prepare the COQ container

coq-chick-blog.opam

@@ -23,6 +23,9 @@ depends: [
   "ocaml"
   "ocamlfind" {build}
 ]
+conflicts: [
+  "ocaml-secondary-compiler"
+]
 tags: [
   "keyword:blog"
   "keyword:effects"

src/Main.v

@@ -1,6 +1,7 @@
 (** The main function (the server handler) and the controller. *)
 Require Import Coq.Lists.List.
 Require Import Coq.NArith.NArith.
+Require Import Coq.Strings.Ascii.
 Require Import Coq.Strings.String.
 Require Import ErrorHandlers.All.
 Require Import FunctionNinjas.All.
@@ -14,6 +15,7 @@ Require Response.
 
 Import ListNotations.
 Import C.Notations.
+Local Open Scope char.
 Local Open Scope string.
 Local Open Scope list.
 

src/Model.v

@@ -3,12 +3,14 @@ Require Import Coq.Bool.Bool.
 Require Import Coq.Lists.List.
 Require Import Coq.NArith.NArith.
 Require Import Coq.Strings.Ascii.
+Require Import Coq.Strings.String.
 Require Import ErrorHandlers.All.
 Require Import FunctionNinjas.All.
 Require Import ListString.All.
 Require Import Moment.All.
 
 Import ListNotations.
+Local Open Scope string.
 Local Open Scope char.
 
 (** A post from the user. *)

src/Render.v

@@ -1,14 +1,15 @@
 (** Pretty-print responses to HTML. *)
 Require Import Coq.Lists.List.
-Require Import Coq.Strings.Ascii.
+Require Import Coq.Strings.String.
 Require Import FunctionNinjas.All.
 Require Import ListString.All.
 Require Http.
 Require Import Model.
 Require Response.
 
 Import ListNotations.
-Local Open Scope char.
+Local Open Scope string.
+Local Open Scope list.
 
 (** The header of a page with the authentication status (logged in or out). *)
 Definition header (is_logged : option bool) : LString.t :=

src/Spec.v

@@ -1,6 +1,7 @@
 (** Specifications. *)
 Require Import Coq.Lists.List.
 Require Import Coq.Strings.Ascii.
+Require Import Coq.Strings.String.
 Require Import FunctionNinjas.All.
 Require Import ListString.All.
 Require Import Computation.
@@ -11,6 +12,8 @@ Require Request.
 
 Import ListNotations.
 Local Open Scope char.
+Local Open Scope string.
+Local Open Scope list.
 Local Set Asymmetric Patterns.
 
 (** A run is an execution of the program with explicit answers for the