Merge pull request #644 from formal-land/guillaume-claret@upgrade-to-coq-8.20

ci: upgrade to Coq 8.20

Author: clarus

.github/workflows/rust.yml

@@ -20,7 +20,7 @@ jobs:
       run: git submodule update --init --recursive
     - uses: coq-community/docker-coq-action@v1
       with:
-        custom_image: coqorg/coq:8.17-ocaml-4.14-flambda
+        custom_image: coqorg/coq:8.20-ocaml-4.14-flambda
         custom_script: |
           startGroup "Install dependencies"
             curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y

CoqOfRust/RecordUpdate.v

@@ -15,7 +15,7 @@ Ltac2 rec strip_foralls (t : constr) :=
 
 Ltac2 app_arg_count (t : constr) :=
   match Constr.Unsafe.kind t with
-  | Constr.Unsafe.App f args => Array.length args
+  | Constr.Unsafe.App _ args => Array.length args
   | _ => 0
   end.
 
@@ -31,7 +31,7 @@ Ltac2 field_names (ctor_ref : Std.reference) :=
 
 Ltac2 constructor_of_record (t : constr) :=
   match Constr.Unsafe.kind t with
-  | Constr.Unsafe.Ind ind inst =>
+  | Constr.Unsafe.Ind ind _ =>
     Std.ConstructRef (Constr.Unsafe.constructor ind 0)
   | _ => Control.throw (Invalid_argument (Some (Message.of_constr t)))
   end.
@@ -44,7 +44,7 @@ Ltac2 record_with_set_val (ty : constr) (record : constr)
   let (h, args) :=
     match Constr.Unsafe.kind ty with
     | Constr.Unsafe.App h args => (h, args)
-    | _ => (ty, Array.empty ())
+    | _ => (ty, Array.empty)
     end in
   let ctor := constructor_of_record h in
   let getters := List.map (fun getterRef =>
@@ -72,8 +72,6 @@ Class Setter{R E: Type}(getter: R -> E): Type :=
   set : E -> R -> R.
 
 Arguments set {R E} (getter) {Setter} (fieldUpdater) (r).
-(* Reduce when calling the [cbn] tactic *)
-Arguments set /.
 
 Global Hint Extern 1 (@Setter ?R ?E ?getter) =>
   exact_setter R getter : typeclass_instances.

CoqOfRust/coq-of-rust.opam

@@ -9,15 +9,15 @@ maintainer: "Guillaume Claret <dev@clarus.me>"
 authors: [
   "Formal Land <contact@formal.land>"
 ]
-license: "AGPL-3.0"
+license: "MIT"
 homepage: "https://formal.land/docs/coq-of-rust/introduction"
 bug-reports: "https://github.com/formal-land/coq-of-rust/issues"
 dev-repo: "git+https://github.com/formal-land/coq-of-rust.git"
 depends: [
-  "ocaml" {>= "4.08"}
-  "coq" {>= "8.17.1" & < "8.18"}
-  "coq-hammer" {>= "1.3.2+8.17" & < "1.3.2+8.18"}
+  "coq" {>= "8.20.0" & < "8.21"}
+  "coq-hammer"
   "coq-coqutil" {>= "0.0.5"}
+  "ocaml" {>= "4.08"}
 ]
 build: [
   [make]

CoqOfRust/links/M.v

@@ -299,7 +299,7 @@ Definition output_with_exception (Output : Set) `{Link Output} (output : Output
   end.
 
 Module Run.
-  Reserved Notation "{{ e ⇓ output_to_value }}" (at level 70, no associativity).
+  Reserved Notation "{{ e ⇓ output_to_value }}" (no associativity).
 
   (** The [Run.t] predicate to show that there exists a trace of execution for an expression [e]
       if we choose the right types/`to_value` functions and make a valid names and traits

CoqOfRust/move_sui/proofs/move_abstract_stack/lib.v

@@ -349,7 +349,7 @@ Module AbstractStack.
           destruct  AbstractStack.pop_any_n_helper as [values'|]; cbn; [|exact I].
           destruct IHvalues' as [items [H_items_len H_items_eq]].
           exists (List.repeat last (Z.to_nat count) ++ items); split.
-          { rewrite List.app_length, List.repeat_length, H_items_len.
+          { rewrite List.length_app, List.repeat_length, H_items_len.
             rewrite Z2Nat.inj_sub; lia.
           }
           { rewrite <- List.app_assoc; f_equal.

CoqOfRust/simulations/M.v

@@ -7,8 +7,8 @@ Module Result.
   | Ok : A -> t A Error
   | Err : Error -> t A Error.
 
-  Arguments Ok {A Error}%type_scope.
-  Arguments Err {A Error}%type_scope.
+  Arguments Ok {A Error}%_type_scope.
+  Arguments Err {A Error}%_type_scope.
 
   Definition return_ {A Error : Set} (value : A) : t A Error := Ok value.