Update MenhirLib to version 20231231

10 files changed, 108 insertions, 128 deletions

diff --git a/MenhirLib/Alphabet.v b/MenhirLib/Alphabet.v
index 8381c01..beaa326 100644
--- a/MenhirLib/Alphabet.v
+++ b/MenhirLib/Alphabet.v
@@ -1,15 +1,13 @@
-(****************************************************************************)
-(*                                                                          *)
-(*                                   Menhir                                 *)
-(*                                                                          *)
-(*           Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud         *)
-(*                                                                          *)
-(*  Copyright Inria. All rights reserved. This file is distributed under    *)
-(*  the terms of the GNU Lesser General Public License as published by the  *)
-(*  Free Software Foundation, either version 3 of the License, or (at your  *)
-(*  option) any later version, as described in the file LICENSE.            *)
-(*                                                                          *)
-(****************************************************************************)
+(******************************************************************************)
+(*                                                                            *)
+(*                                   Menhir                                   *)
+(*                                                                            *)
+(*  Copyright Inria and CNRS. All rights reserved. This file is distributed   *)
+(*  under the terms of the GNU Lesser General Public License as published by  *)
+(*  the Free Software Foundation, either version 3 of the License, or (at     *)
+(*  your option) any later version, as described in the file LICENSE.         *)
+(*                                                                            *)
+(******************************************************************************)
 
 From Coq Require Import ZArith List Relations RelationClasses.
 Import ListNotations.
@@ -75,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/MenhirLib/Automaton.v b/MenhirLib/Automaton.v
index 1975be4..24919f2 100644
--- a/MenhirLib/Automaton.v
+++ b/MenhirLib/Automaton.v
@@ -1,15 +1,13 @@
-(****************************************************************************)
-(*                                                                          *)
-(*                                   Menhir                                 *)
-(*                                                                          *)
-(*           Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud         *)
-(*                                                                          *)
-(*  Copyright Inria. All rights reserved. This file is distributed under    *)
-(*  the terms of the GNU Lesser General Public License as published by the  *)
-(*  Free Software Foundation, either version 3 of the License, or (at your  *)
-(*  option) any later version, as described in the file LICENSE.            *)
-(*                                                                          *)
-(****************************************************************************)
+(******************************************************************************)
+(*                                                                            *)
+(*                                   Menhir                                   *)
+(*                                                                            *)
+(*  Copyright Inria and CNRS. All rights reserved. This file is distributed   *)
+(*  under the terms of the GNU Lesser General Public License as published by  *)
+(*  the Free Software Foundation, either version 3 of the License, or (at     *)
+(*  your option) any later version, as described in the file LICENSE.         *)
+(*                                                                            *)
+(******************************************************************************)
 
 Require Grammar.
 Require Export Alphabet.
diff --git a/MenhirLib/Grammar.v b/MenhirLib/Grammar.v
index 35ccbd8..1837b87 100644
--- a/MenhirLib/Grammar.v
+++ b/MenhirLib/Grammar.v
@@ -1,15 +1,13 @@
-(****************************************************************************)
-(*                                                                          *)
-(*                                   Menhir                                 *)
-(*                                                                          *)
-(*           Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud         *)
-(*                                                                          *)
-(*  Copyright Inria. All rights reserved. This file is distributed under    *)
-(*  the terms of the GNU Lesser General Public License as published by the  *)
-(*  Free Software Foundation, either version 3 of the License, or (at your  *)
-(*  option) any later version, as described in the file LICENSE.            *)
-(*                                                                          *)
-(****************************************************************************)
+(******************************************************************************)
+(*                                                                            *)
+(*                                   Menhir                                   *)
+(*                                                                            *)
+(*  Copyright Inria and CNRS. All rights reserved. This file is distributed   *)
+(*  under the terms of the GNU Lesser General Public License as published by  *)
+(*  the Free Software Foundation, either version 3 of the License, or (at     *)
+(*  your option) any later version, as described in the file LICENSE.         *)
+(*                                                                            *)
+(******************************************************************************)
 
 From Coq Require Import List Orders.
 Import ListNotations.
diff --git a/MenhirLib/Interpreter.v b/MenhirLib/Interpreter.v
index 922d665..6ae6eda 100644
--- a/MenhirLib/Interpreter.v
+++ b/MenhirLib/Interpreter.v
@@ -1,15 +1,13 @@
-(****************************************************************************)
-(*                                                                          *)
-(*                                   Menhir                                 *)
-(*                                                                          *)
-(*           Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud         *)
-(*                                                                          *)
-(*  Copyright Inria. All rights reserved. This file is distributed under    *)
-(*  the terms of the GNU Lesser General Public License as published by the  *)
-(*  Free Software Foundation, either version 3 of the License, or (at your  *)
-(*  option) any later version, as described in the file LICENSE.            *)
-(*                                                                          *)
-(****************************************************************************)
+(******************************************************************************)
+(*                                                                            *)
+(*                                   Menhir                                   *)
+(*                                                                            *)
+(*  Copyright Inria and CNRS. All rights reserved. This file is distributed   *)
+(*  under the terms of the GNU Lesser General Public License as published by  *)
+(*  the Free Software Foundation, either version 3 of the License, or (at     *)
+(*  your option) any later version, as described in the file LICENSE.         *)
+(*                                                                            *)
+(******************************************************************************)
 
 From Coq Require Import List Syntax.
 Import ListNotations.
@@ -84,8 +82,8 @@ CoInductive buffer : Type :=
   Buf_cons { buf_head : token; buf_tail : buffer }.
 
 (* Note: Coq 8.12.0 wants a Declare Scope command,
-   but this breaks compatibility with Coq < 8.10. *)
-Declare Scope buffer_scope.
+   but this breaks compatibility with Coq < 8.10.
+   Declare Scope buffer_scope. *)
 Delimit Scope buffer_scope with buf.
 Bind Scope buffer_scope with buffer.
 
diff --git a/MenhirLib/Interpreter_complete.v b/MenhirLib/Interpreter_complete.v
index 51f2524..10d5cb7 100644
--- a/MenhirLib/Interpreter_complete.v
+++ b/MenhirLib/Interpreter_complete.v
@@ -1,15 +1,13 @@
-(****************************************************************************)
-(*                                                                          *)
-(*                                   Menhir                                 *)
-(*                                                                          *)
-(*           Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud         *)
-(*                                                                          *)
-(*  Copyright Inria. All rights reserved. This file is distributed under    *)
-(*  the terms of the GNU Lesser General Public License as published by the  *)
-(*  Free Software Foundation, either version 3 of the License, or (at your  *)
-(*  option) any later version, as described in the file LICENSE.            *)
-(*                                                                          *)
-(****************************************************************************)
+(******************************************************************************)
+(*                                                                            *)
+(*                                   Menhir                                   *)
+(*                                                                            *)
+(*  Copyright Inria and CNRS. All rights reserved. This file is distributed   *)
+(*  under the terms of the GNU Lesser General Public License as published by  *)
+(*  the Free Software Foundation, either version 3 of the License, or (at     *)
+(*  your option) any later version, as described in the file LICENSE.         *)
+(*                                                                            *)
+(******************************************************************************)
 
 From Coq Require Import List Arith.
 Import ListNotations.
@@ -788,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
@@ -816,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.
 
diff --git a/MenhirLib/Interpreter_correct.v b/MenhirLib/Interpreter_correct.v
index 083be5b..645d067 100644
--- a/MenhirLib/Interpreter_correct.v
+++ b/MenhirLib/Interpreter_correct.v
@@ -1,15 +1,13 @@
-(****************************************************************************)
-(*                                                                          *)
-(*                                   Menhir                                 *)
-(*                                                                          *)
-(*           Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud         *)
-(*                                                                          *)
-(*  Copyright Inria. All rights reserved. This file is distributed under    *)
-(*  the terms of the GNU Lesser General Public License as published by the  *)
-(*  Free Software Foundation, either version 3 of the License, or (at your  *)
-(*  option) any later version, as described in the file LICENSE.            *)
-(*                                                                          *)
-(****************************************************************************)
+(******************************************************************************)
+(*                                                                            *)
+(*                                   Menhir                                   *)
+(*                                                                            *)
+(*  Copyright Inria and CNRS. All rights reserved. This file is distributed   *)
+(*  under the terms of the GNU Lesser General Public License as published by  *)
+(*  the Free Software Foundation, either version 3 of the License, or (at     *)
+(*  your option) any later version, as described in the file LICENSE.         *)
+(*                                                                            *)
+(******************************************************************************)
 
 From Coq Require Import List.
 Import ListNotations.
diff --git a/MenhirLib/Main.v b/MenhirLib/Main.v
index f615807..4469d2a 100644
--- a/MenhirLib/Main.v
+++ b/MenhirLib/Main.v
@@ -1,15 +1,13 @@
-(****************************************************************************)
-(*                                                                          *)
-(*                                   Menhir                                 *)
-(*                                                                          *)
-(*           Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud         *)
-(*                                                                          *)
-(*  Copyright Inria. All rights reserved. This file is distributed under    *)
-(*  the terms of the GNU Lesser General Public License as published by the  *)
-(*  Free Software Foundation, either version 3 of the License, or (at your  *)
-(*  option) any later version, as described in the file LICENSE.            *)
-(*                                                                          *)
-(****************************************************************************)
+(******************************************************************************)
+(*                                                                            *)
+(*                                   Menhir                                   *)
+(*                                                                            *)
+(*  Copyright Inria and CNRS. All rights reserved. This file is distributed   *)
+(*  under the terms of the GNU Lesser General Public License as published by  *)
+(*  the Free Software Foundation, either version 3 of the License, or (at     *)
+(*  your option) any later version, as described in the file LICENSE.         *)
+(*                                                                            *)
+(******************************************************************************)
 
 Require Grammar Automaton Interpreter_correct Interpreter_complete.
 From Coq Require Import Syntax Arith.
diff --git a/MenhirLib/Validator_classes.v b/MenhirLib/Validator_classes.v
index cced28a..f96f3e2 100644
--- a/MenhirLib/Validator_classes.v
+++ b/MenhirLib/Validator_classes.v
@@ -1,15 +1,13 @@
-(****************************************************************************)
-(*                                                                          *)
-(*                                   Menhir                                 *)
-(*                                                                          *)
-(*           Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud         *)
-(*                                                                          *)
-(*  Copyright Inria. All rights reserved. This file is distributed under    *)
-(*  the terms of the GNU Lesser General Public License as published by the  *)
-(*  Free Software Foundation, either version 3 of the License, or (at your  *)
-(*  option) any later version, as described in the file LICENSE.            *)
-(*                                                                          *)
-(****************************************************************************)
+(******************************************************************************)
+(*                                                                            *)
+(*                                   Menhir                                   *)
+(*                                                                            *)
+(*  Copyright Inria and CNRS. All rights reserved. This file is distributed   *)
+(*  under the terms of the GNU Lesser General Public License as published by  *)
+(*  the Free Software Foundation, either version 3 of the License, or (at     *)
+(*  your option) any later version, as described in the file LICENSE.         *)
+(*                                                                            *)
+(******************************************************************************)
 
 From Coq Require Import List.
 From Coq.ssr Require Import ssreflect.
diff --git a/MenhirLib/Validator_complete.v b/MenhirLib/Validator_complete.v
index 4b4d127..8875f11 100644
--- a/MenhirLib/Validator_complete.v
+++ b/MenhirLib/Validator_complete.v
@@ -1,15 +1,13 @@
-(****************************************************************************)
-(*                                                                          *)
-(*                                   Menhir                                 *)
-(*                                                                          *)
-(*           Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud         *)
-(*                                                                          *)
-(*  Copyright Inria. All rights reserved. This file is distributed under    *)
-(*  the terms of the GNU Lesser General Public License as published by the  *)
-(*  Free Software Foundation, either version 3 of the License, or (at your  *)
-(*  option) any later version, as described in the file LICENSE.            *)
-(*                                                                          *)
-(****************************************************************************)
+(******************************************************************************)
+(*                                                                            *)
+(*                                   Menhir                                   *)
+(*                                                                            *)
+(*  Copyright Inria and CNRS. All rights reserved. This file is distributed   *)
+(*  under the terms of the GNU Lesser General Public License as published by  *)
+(*  the Free Software Foundation, either version 3 of the License, or (at     *)
+(*  your option) any later version, as described in the file LICENSE.         *)
+(*                                                                            *)
+(******************************************************************************)
 
 From Coq Require Import List Syntax Derive.
 From Coq.ssr Require Import ssreflect.
diff --git a/MenhirLib/Validator_safe.v b/MenhirLib/Validator_safe.v
index 0f32ea5..c6a3d71 100644
--- a/MenhirLib/Validator_safe.v
+++ b/MenhirLib/Validator_safe.v
@@ -1,15 +1,13 @@
-(****************************************************************************)
-(*                                                                          *)
-(*                                   Menhir                                 *)
-(*                                                                          *)
-(*           Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud         *)
-(*                                                                          *)
-(*  Copyright Inria. All rights reserved. This file is distributed under    *)
-(*  the terms of the GNU Lesser General Public License as published by the  *)
-(*  Free Software Foundation, either version 3 of the License, or (at your  *)
-(*  option) any later version, as described in the file LICENSE.            *)
-(*                                                                          *)
-(****************************************************************************)
+(******************************************************************************)
+(*                                                                            *)
+(*                                   Menhir                                   *)
+(*                                                                            *)
+(*  Copyright Inria and CNRS. All rights reserved. This file is distributed   *)
+(*  under the terms of the GNU Lesser General Public License as published by  *)
+(*  the Free Software Foundation, either version 3 of the License, or (at     *)
+(*  your option) any later version, as described in the file LICENSE.         *)
+(*                                                                            *)
+(******************************************************************************)
 
 From Coq Require Import List Syntax Derive.
 Import ListNotations.