Merge pull request #8 from coq-community/fix-deprec-8.16

Fix deprec 8.16

.github/workflows/docker-action.yml

@@ -18,12 +18,12 @@ jobs:
  matrix:
  image:
  - 'coqorg/coq:dev'
+ - 'coqorg/coq:8.16'
  - 'coqorg/coq:8.15'
  - 'coqorg/coq:8.14'
  - 'coqorg/coq:8.13'
  - 'coqorg/coq:8.12'
  - 'coqorg/coq:8.11'
- - 'coqorg/coq:8.10'
  fail-fast: false
  steps:
  - uses: actions/checkout@v2

README.md

@@ -42,7 +42,7 @@ Theorem, useful for proving termination.
 - Coq-community maintainer(s):
  - Karl Palmskog ([**@palmskog**](https://github.com/palmskog))
 - License: [MIT License](LICENSE)
-- Compatible Coq versions: 8.10 or later
+- Compatible Coq versions: 8.11 or later
 - Additional dependencies: none
 - Coq namespace: `AlmostFull`
 - Related publication(s):

coq-almost-full.opam

@@ -18,7 +18,7 @@ Theorem, useful for proving termination."""
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
  "dune" {>= "2.5"}
- "coq" {(>= "8.10" & < "8.16~") | (= "dev")}
+ "coq" {(>= "8.11" & < "8.17~") | (= "dev")}
 ]
 
 tags: [

meta.yml

@@ -42,20 +42,20 @@ license:
  identifier: MIT
 
 supported_coq_versions:
- text: 8.10 or later
- opam: '{(>= "8.10" & < "8.16~") | (= "dev")}'
+ text: 8.11 or later
+ opam: '{(>= "8.11" & < "8.17~") | (= "dev")}'
 
 tested_coq_nix_versions:
 - coq_version: 'master'
 
 tested_coq_opam_versions:
 - version: dev
+- version: '8.16'
 - version: '8.15'
 - version: '8.14'
 - version: '8.13'
 - version: '8.12'
 - version: '8.11'
-- version: '8.10'
 
 namespace: AlmostFull
 

theories/Default/AlmostFull.v

@@ -113,12 +113,14 @@ Lemma le_tree_rewrite_aux :
  forall n x, n > x -> ltree_aux n x = le_tree x.
 Proof.
 intro n. induction n. intros. inversion H.
-intros. destruct (gt_S _ _ H). simpl. 
+intros. 
+destruct ((proj1 (Nat.lt_eq_cases _ _)) (proj2 (Nat.succ_le_mono _ _) H)).
+simpl.
 unfold le_tree. simpl. apply sup_eq. 
-apply functional_extensionality. intro y. 
+apply functional_extensionality. intro y.
 destruct (le_lt_dec x y). auto. 
 apply aux_le_tree_aux. lia. lia.
-rewrite H0. unfold le_tree. reflexivity. 
+rewrite H0. unfold le_tree. reflexivity.
 Qed.
 
 Lemma le_tree_rewrite : forall (x:nat),

theories/Default/AlmostFullInduction.v

@@ -328,7 +328,7 @@ destruct kx.
  intros. apply (X0 (@FinIntro k (k-1) H0,y)). simpl. 
  unfold lift_diag. unfold fst. unfold snd. split. unfold next_fin. lia. apply H.
  (* Now it is an (S kx) *) 
- assert (kx < k). intuition; lia.
+ assert (kx < k). intuition auto; lia.
  intros. apply (X0 (@FinIntro k kx H0,y)). simpl. unfold lift_diag. simpl. split. 
  simpl. unfold next_fin. right. intuition lia. apply H.
 (* Show the goal *)

theories/PropBounded/AlmostFullInduction.v

@@ -321,8 +321,8 @@ destruct kx.
  assert (k-1 < k). lia.
  intros. apply (X0 (@FinIntro k (k-1) H0,y)). simpl. 
  unfold lift_diag. unfold fst. unfold snd. split. unfold next_fin. lia. apply H.
- (* Now it is an (S kx) *) 
- assert (kx < k). intuition; lia.
+ (* Now it is an (S kx) *)
+ assert (kx < k). intuition auto; lia.
  intros. apply (X0 (@FinIntro k kx H0,y)). simpl. unfold lift_diag. simpl. split. 
  simpl. unfold next_fin. right. intuition lia. apply H.
 (* Show the goal *)