Bump the recommended OCaml version to 4.14.2 (master branch)

README.md

@@ -120,7 +120,7 @@ You can use `opam` to install the current state of this branch as follows.
 We recommend creating a fresh opam switch:
 
 ```
-opam switch create coq-library-undecidability --packages=ocaml-variants.4.14.1+options,ocaml-option-flambda
+opam switch create coq-library-undecidability --packages=ocaml-variants.4.14.2+options,ocaml-option-flambda
 eval $(opam env)
 ```
 
@@ -129,15 +129,15 @@ Then the following commands install the library:
 ```
 opam repo add coq-released https://coq.inria.fr/opam/released
 opam update
-opam pin add coq-library-undecidability.dev+9.0 "https://github.com/uds-psl/coq-library-undecidability.git#rocq-9.0"
+opam pin add coq-library-undecidability.dev+9.2 "https://github.com/uds-psl/coq-library-undecidability.git#rocq-9.2"
 ```
 
 ### Manual installation
 
-You need `Rocq 9.0` built on OCAML `>= 4.09.1` (but we recommend and test OCaml version `4.14.1+flambda`) and the Template-Coq part of the [MetaCoq](https://metacoq.github.io/) package for Coq. If you are using `opam 2` you can use the following commands to install the dependencies on a new switch:
+You need `Rocq 9.2` built on OCAML `>= 4.09.1` (but we recommend and test OCaml version `4.14.2+flambda`) and the Template-Coq part of the [MetaCoq](https://metacoq.github.io/) package for Coq. If you are using `opam 2` you can use the following commands to install the dependencies on a new switch:
 
 ```
-opam switch create coq-library-undecidability --packages=ocaml-variants.4.14.1+options,ocaml-option-flambda
+opam switch create coq-library-undecidability --packages=ocaml-variants.4.14.2+options,ocaml-option-flambda
 eval $(opam env)
 opam repo add rocq-released https://rocq-prover.org/opam/released
 opam update
@@ -162,7 +162,7 @@ The library is compatible with Coq's compiled interfaces ([`vos`](https://coq.in
 
 #### Coq version
 
-Be careful that this branch only compiles under `Coq 8.16`. If you want to use a different Coq version you have to change to a different branch.
+Be careful that this branch only compiles under `Rocq 9.2`. If you want to use a different Coq version you have to change to a different branch.
 Due to compatibility issues, not every branch contains exactly the same problems. 
 We recommend to use the newest branch if possible.
 

theories/FOL/TRAKHTENBROT/enumerable.v

@@ -130,7 +130,7 @@ Section enumerable_definitions.
 
     Theorem type_enum_t_by_measure : type_enum_t.
     Proof using Hm.
-      apply constructive_choice in Hm; destruct Hm as (f & Hf); clear Hm.
+      apply constructive_choice in Hm; destruct Hm as (f & Hf).
       exists (fun j => let (a,n) := surj j in f a n).
       intros x.
       destruct (proj1 (Hf _ x) (Nat.le_refl _)) as (a & Ha).

theories/HOU/firstorder.v

@@ -920,7 +920,7 @@ Section FirstOrderDecidable.
 
 
 
-  Let free (k: nat) (x: nat) := x >= k.
+  Local Definition free (k: nat) (x: nat) := x >= k.
 
   Instance dec_free k: Dec1 (free k).
   Proof. unfold free; typeclasses eauto. Qed.
@@ -1024,7 +1024,7 @@ Section FirstOrderDecidable.
       * specialize decr_typing with (L := rev L) as H9; simplify in H9; eauto. 
       * eapply decr_unifies; eauto.
         specialize (unify_unifiable H' (AppR s T, AppR t T0)); cbn; auto.
-      * eapply lambda_free_normal. pose proof (free := fun (k: nat) (x: nat) => x >= k).
+      * eapply lambda_free_normal.
         eapply decr_lambda_free; intros; eapply LF.
     + intros (Delta & sigma & E1 & E2 & E3).  asimpl in E2. 
       eapply Lambda_injective in E2.
@@ -1057,4 +1057,4 @@ Section FirstOrderDecidable.
   Qed.
 
 End FirstOrderDecidable.
-
+