fix deprecations in Coq and OCaml

Author: palmskog

Makefile

@@ -1,4 +1,4 @@
-OCAMLBUILD = ocamlbuild -tag safe_string -libs unix -I shims
+OCAMLBUILD = ocamlbuild -tag safe_string -pkg unix -I shims
 
 default: Makefile.coq
 	$(MAKE) -f Makefile.coq

_CoqProject

@@ -6,7 +6,6 @@
 -arg -w -arg -projection-no-head-constant
 -arg -w -arg -duplicate-clear
 -arg -w -arg -notation-incompatible-format
--arg -w -arg -deprecated-hint-without-locality
 
 theories/Core/State.v
 theories/Core/Freshness.v

theories/Core/HoareTriples.v

@@ -12,7 +12,7 @@ Unset Printing Implicit Defensive.
 Structure prog (W : world) A (this : nid) :=
   Prog {
       set_of : proc this W A -> Prop; 
-      (* Unifinshed is a bottom element that should be present *)
+      (* Unfinished is a bottom element that should be present *)
       _ : set_of Unfinished
   }.
 
@@ -441,7 +441,7 @@ Lemma conseq_refl (W : world) A this (e : DT this W A) :
   conseq e (spec_of e).
 Proof. by case: e; case=>p q [T H i] /= Hp C t; apply: H. Qed.
 
-Hint Resolve conseq_refl : core.
+#[export] Hint Resolve conseq_refl : core.
 
 
 (* Weakening the specifications *)

theories/Core/dune

@@ -8,5 +8,4 @@
    -w -local-declaration
    -w -duplicate-clear
    -w -redundant-canonical-projection
-   -w -projection-no-head-constant
-   -w -deprecated-hint-without-locality))
+   -w -projection-no-head-constant))