search

coq-community / reduction-effects

A Coq plugin to add reduction side effects to some Coq reduction strategies [maintainers=@liyishuai,@JasonGross]
Mozilla Public License 2.0
6 stars 6 forks source link

Support for Coq 8.18 #19

Closed SnarkBoojum closed 1 year ago

SnarkBoojum commented 1 year ago

I tried to compile with 8.18, and had to make the following modification to make it work:

--- coq-reduction-effects.orig/redeffect.mlg
+++ coq-reduction-effects/redeffect.mlg
@@ -47,7 +47,7 @@
   | _ -> CErrors.user_err (Pp.strbrk "Printing function should be a constant.")

 let printing_hook env sigma c =
-  let (f,l) = Constr.decompose_appvect c in
+  let (f,l) = Constr.decompose_app c in
   if Array.length l >= 2 then
     Feedback.msg_notice (Printer.pr_constr_env env sigma (l.(1)))
liyishuai commented 1 year ago

Done by #17 I'll release it on OPAM today.

liyishuai commented 1 year ago

Tagged: https://github.com/coq-community/reduction-effects/releases/tag/v0.1.5

liyishuai commented 1 year ago 
opam install coq-reduction-effects.0.1.5
SnarkBoojum commented 1 year ago

Thanks -- notice I'm the Debian developer packaging coq-reduction-effects, so I use the tag on the repository and not opam.