Adapt to coq/coq#18164

This merges MR #36.
LexiFi · Oct 24, 2023 · 673fe6d · 673fe6d
1 parent 5a7c689
commit 673fe6d
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 6 deletions.
diff --git a/coq-menhirlib/src/Alphabet.v b/coq-menhirlib/src/Alphabet.v
@@ -73,7 +73,7 @@ rewrite Nat.compare_eq_iff in *; destruct H; assumption.
 rewrite <- nat_compare_lt in *.
 apply (Nat.lt_trans _ _ _ H H0).
 rewrite <- nat_compare_gt in *.
-apply (gt_trans _ _ _ H H0).
+apply (Nat.lt_trans _ _ _ H0 H).
 Qed.
 
 (** A pair of comparable is comparable. **)

diff --git a/coq-menhirlib/src/Interpreter_complete.v b/coq-menhirlib/src/Interpreter_complete.v
@@ -786,9 +786,9 @@ Proof.
   - assert (Hptd := next_ptd_cost ptd). destruct next_ptd=>//. by rewrite Hptd.
   - rewrite Nat.add_0_r. assert (IH1 := IH ptd). destruct next_ptd_iter as [ptd'|].
     + specialize (IH ptd'). destruct next_ptd_iter as [ptd''|].
-      * by rewrite IH1 IH -!plus_assoc.
-      * rewrite IH1. by apply plus_lt_compat_l.
-    + by apply lt_plus_trans.
+      * by rewrite IH1 IH -!Nat.add_assoc.
+      * rewrite IH1. by apply Nat.add_lt_mono_l.
+    + by apply Nat.lt_le_trans with (1 := IH1), Nat.le_add_r.
 Qed.
 
 (** We now prove the top-level parsing function. The only thing that
@@ -814,8 +814,8 @@ Proof.
   destruct next_ptd_iter.
   - destruct Hparse as (? & -> & ?). apply (f_equal S) in Hcost.
     rewrite -ptd_cost_build_from_pt Nat.add_0_r in Hcost. rewrite Hcost.
-    apply le_lt_n_Sm, le_plus_l.
-  - rewrite Hparse. split; [|split]=>//. apply lt_le_S in Hcost.
+    apply Nat.lt_succ_r, Nat.le_add_r.
+  - rewrite Hparse. split; [|split]=>//. apply Nat.le_succ_l in Hcost.
     by rewrite -ptd_cost_build_from_pt Nat.add_0_r in Hcost.
 Qed.