Merge pull request #67 from pi8027/coq-8.12

coq-ott compatible with Coq 8.12
ott-lang · Aug 19, 2020 · 5ded0b0 · 5ded0b0
2 parents 0d28d66 + 672beb0
commit 5ded0b0
Show file tree

Hide file tree

Showing 4 changed files with 5 additions and 2 deletions.
diff --git a/coq-ott.opam b/coq-ott.opam
@@ -17,7 +17,7 @@ this library.
 build: [make "-j%{jobs}%" "-C" "coq"]
 install: [make "-C" "coq" "install"]
 depends: [
-  "coq" {(>= "8.5" & < "8.12~") | (= "dev")}
+  "coq" {(>= "8.5" & < "8.13~") | (= "dev")}
 ]
 tags: [
   "category:Computer Science/Semantics and Compilation/Semantics"

diff --git a/coq/.gitignore b/coq/.gitignore
@@ -1,6 +1,7 @@
 *.vo
 *.vio
 *.vos
+*.vok
 *.glob
 *.v.d
 *.aux

diff --git a/coq/_CoqProject b/coq/_CoqProject
@@ -12,3 +12,5 @@ ott_list_nth.v
 ott_list_core.v
 ott_list_distinct.v
 ott_list_flat_map.v
+
+-arg -w -arg -omega-is-deprecated
diff --git a/coq/ott_list_predicate.v b/coq/ott_list_predicate.v
@@ -59,7 +59,7 @@ Qed.
 Lemma In_Forall_list :
   forall P l, (forall x, In x l -> P x) -> Forall_list P l.
 Proof.
-  induction l; firstorder.
+  induction l; constructor; firstorder.
 Qed.
 
 Lemma exists_In_Exists_list :
-Original file line number
+Diff line change
@@ -1,6 +1,7 @@
     *.vo
     *.vio
     *.vos
+    *.vok
     *.glob
     *.v.d
     *.aux
@@ Expand Down @@