From ec83caca2cd793ca69e199a757251af21e4af424 Mon Sep 17 00:00:00 2001 From: Kenji Maillard Date: Sat, 23 Dec 2023 19:43:24 +0100 Subject: [PATCH 1/2] update summary declaration to 8.18 --- src/smpl.mlg | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smpl.mlg b/src/smpl.mlg index 93e1e98..75cb0dc 100644 --- a/src/smpl.mlg +++ b/src/smpl.mlg @@ -38,7 +38,7 @@ let smpl_dbs = ref (StringMap.empty : smpl_db StringMap.t) (*** Summary ***) let init () = smpl_dbs := StringMap.empty -let freeze ~marshallable = !smpl_dbs +let freeze () = !smpl_dbs let unfreeze t = smpl_dbs := t let _ = Summary.declare_summary "smpl" From e6a21f2570b64436e2594bd7c51f334027318eaf Mon Sep 17 00:00:00 2001 From: Kenji Maillard Date: Thu, 25 Jan 2024 11:59:19 +0100 Subject: [PATCH 2/2] update opam --- opam | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/opam b/opam index a9e3fe3..9eb4897 100644 --- a/opam +++ b/opam @@ -12,7 +12,7 @@ build: [make "-j%{jobs}%"] install: [make "install"] depends: [ "ocaml" - "coq" { >= "8.16" | = "dev" } + "coq" { >= "8.18" | = "dev" } ] synopsis: "Smpl: An Extensible Tactic for Coq" description: """