From 795b964a1b83bd78636a4721ca62b55a5727bedf Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 2 Oct 2024 10:45:44 +0200 Subject: [PATCH] fix compilation on 8.20 --- apps/cs/src/coq_elpi_cs_hook.mlg | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/apps/cs/src/coq_elpi_cs_hook.mlg b/apps/cs/src/coq_elpi_cs_hook.mlg index d52b8a26f..7fb485a03 100644 --- a/apps/cs/src/coq_elpi_cs_hook.mlg +++ b/apps/cs/src/coq_elpi_cs_hook.mlg @@ -62,6 +62,11 @@ open Elpi_plugin open Coq_elpi_arg_syntax open Coq_elpi_vernacular +[%%if coq = "8.20"] +let adapt_hook f : Evarconv.hook = fun env sigma (s,l,t) x -> f env sigma (s,Some l,t) x +[%%else] +let adapt_hook f : Evarconv.hook = f +[%%endif] let add_cs_hook = let cs_hook_program = Summary.ref ~name:"elpi-cs" None in @@ -70,7 +75,7 @@ let add_cs_hook = | None -> None | Some h -> elpi_cs_hook h env sigma proj pat in let name = "elpi-cs" in - Evarconv.register_hook ~name cs_hook; + Evarconv.register_hook ~name (adapt_hook cs_hook); let inCs = let cache program = cs_hook_program := Some program;