Force OCaml >= 5.3

.github/workflows/ci.yml

@@ -21,8 +21,8 @@ jobs:
     - uses: actions/checkout@v4
     - name: Install EasyCrypt dependencies
       run: |
-        opam pin add -n easycrypt .
-        opam install --deps-only easycrypt
+        opam pin add --update-invariant -n easycrypt .
+        opam install --update-invariant --deps-only easycrypt
     - name: Compile EasyCrypt
       run: opam exec -- make PROFILE=ci
 
@@ -60,8 +60,8 @@ jobs:
     - uses: actions/checkout@v4
     - name: Install EasyCrypt dependencies
       run: |
-        opam pin add -n easycrypt .
-        opam install --deps-only easycrypt
+        opam pin add --update-invariant -n easycrypt .
+        opam install --update-invariant --deps-only easycrypt
     - name: Compile EasyCrypt
       run: opam exec -- make
     - name: Detect SMT provers
@@ -127,8 +127,8 @@ jobs:
           project/${{ matrix.target.name }}
     - name: Install EasyCrypt dependencies
       run: |
-        opam pin add -n easycrypt easycrypt
-        opam install --deps-only easycrypt
+        opam pin add --update-invariant -n easycrypt easycrypt
+        opam install --update-invariant --deps-only easycrypt
     - name: Compile & Install EasyCrypt
       run: opam exec -- make -C easycrypt build install
     - name: Detect SMT provers

dune-project

@@ -12,7 +12,7 @@
  (name easycrypt)
  (sites (lib theories) (libexec commands))
  (depends
-  (ocaml (>= 4.08.0))
+  (ocaml (>= 5.3))
   (batteries (>= 3))
   (camlp-streams (>= 5))
   camlzip

easycrypt.opam

@@ -1,6 +1,6 @@
 # This file is generated by dune, edit dune-project instead
 depends: [
-  "ocaml" {>= "4.08.0"}
+  "ocaml" {>= "5.3"}
   "batteries" {>= "3"}
   "camlp-streams" {>= "5"}
   "camlzip"

src/ecAst.ml

@@ -854,8 +854,8 @@ module Hexpr = Why3.Hashcons.Make (struct
     in
     Why3.Hashcons.combine_list b1_hash 0 bs
 
-  let hash e =
-    match e.e_node with
+  let hash_node (e : expr_node) =
+    match e with
     | Eint   i -> BI.hash i
     | Elocal x -> Hashtbl.hash x
     | Evar   x -> pv_hash x
@@ -889,6 +889,9 @@ module Hexpr = Why3.Hashcons.Make (struct
     | Eproj (e, i) ->
         Why3.Hashcons.combine (e_hash e) i
 
+  let hash (e : expr) =
+    Why3.Hashcons.combine (ty_hash e.e_ty) (hash_node e.e_node)
+
   let fv_node e =
     let union ex =
       List.fold_left (fun s e -> fv_union s (ex e)) Mid.empty
@@ -980,8 +983,8 @@ module Hsform = Why3.Hashcons.Make (struct
        ty_equal f1.f_ty f2.f_ty
     && equal_node f1.f_node f2.f_node
 
-  let hash f =
-    match f.f_node with
+  let hash_node (f : f_node) =
+    match f with
     | Fquant(q, b, f) ->
         Why3.Hashcons.combine2 (f_hash f) (b_hash b) (qt_hash q)
 
@@ -1028,6 +1031,9 @@ module Hsform = Why3.Hashcons.Make (struct
     | FeagerF     eg   -> eg_hash eg
     | Fpr         pr   -> pr_hash pr
 
+  let hash (f : form) =
+    Why3.Hashcons.combine (ty_hash f.f_ty) (hash_node f.f_node)
+
   let fv_mlr = Sid.add mleft (Sid.singleton mright)
 
   let fv_node f =