Merge pull request #18 from coq-community/ignore-warnings

Ignore warnings in 8.12
coq-community · Oct 5, 2020 · 62ad0b7 · 62ad0b7
2 parents 39b75d2 + 88906cd
commit 62ad0b7
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 2 deletions.
diff --git a/_CoqProject b/_CoqProject
@@ -1,6 +1,8 @@
 -Q theories RegLang
 -arg -w -arg -notation-overridden
 -arg -w -arg -duplicate-clear
+-arg -w -arg -notation-incompatible-format
+-arg -w -arg -omega-is-deprecated
 theories/misc.v
 theories/setoid_leq.v
 theories/languages.v

diff --git a/theories/dune b/theories/dune
@@ -2,4 +2,4 @@
  (name RegLang)
  (package coq-reglang)
  (synopsis "Representations of regular languages (i.e., regexps, various types of automata, and WS1S) with equivalence proofs, in Coq and MathComp")
- (flags -w -notation-overridden -w -duplicate-clear))
+ (flags -w -notation-overridden -w -duplicate-clear -w -notation-incompatible-format -w -omega-is-deprecated))
diff --git a/theories/misc.v b/theories/misc.v
@@ -28,7 +28,7 @@ Lemma eqb_iff (b1 b2 : bool) : (b1 <-> b2) <-> (b1 = b2).
 Proof. split => [[A B]|->//]. exact/idP/idP. Qed.
 
 (* equivalence of type inhabitation *)
-CoInductive iffT T1 T2 := IffT of (T1 -> T2) & (T2 -> T1).
+Variant iffT T1 T2 := IffT of (T1 -> T2) & (T2 -> T1).
 Notation "T1 <-T-> T2" := (iffT T1 T2) (at level 30).
 
 Definition iffT_LR T1 T2 : iffT T1 T2 -> T1 -> T2. by case. Qed.