From afa139bee64a0e3e1c708712295b32eaf3c5beba Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Fri, 5 Dec 2025 22:31:58 +0100 Subject: [PATCH] Adapt to rocq-prover/rocq#21384. --- template-rocq/src/plugin_core.ml | 3 +-- template-rocq/src/run_template_monad.ml | 3 +-- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/template-rocq/src/plugin_core.ml b/template-rocq/src/plugin_core.ml index 332debcc0..bcd892819 100644 --- a/template-rocq/src/plugin_core.ml +++ b/template-rocq/src/plugin_core.ml @@ -131,8 +131,7 @@ let tmLemma (nm : ident) ?poly:(poly=false)(ty : term) : kername tm = let cinfo = Declare.CInfo.make ~name:nm ~typ:cty () in let info = Declare.Info.make ~poly ~kind () in (* This should register properly with the interpretation extension *) - let pm, _ = Declare.Obls.add_definition ~pm:st ~cinfo ~info ~body:c ~uctx:ctx ~obl_hook ~opaque:false obls in - pm + Declare.Obls.add_definition ~pm:st ~cinfo ~info ~body:c ~uctx:ctx ~obl_hook ~opaque:false obls let tmFreshName (nm : ident) : ident tm = fun ~st env evd success _fail -> diff --git a/template-rocq/src/run_template_monad.ml b/template-rocq/src/run_template_monad.ml index 627047499..a226c060b 100644 --- a/template-rocq/src/run_template_monad.ml +++ b/template-rocq/src/run_template_monad.ml @@ -446,8 +446,7 @@ let rec run_template_program_rec ~poly ?(intactic=false) (k : Constr.t Plugin_co k ~st:pm env evm (EConstr.to_constr evm t)) in (* todo better *) let cinfo = Declare.CInfo.make ~name:ident ~typ:cty () in let info = Declare.Info.make ~poly ~kind () in - let pm, _ = Declare.Obls.add_definition ~pm:st ~cinfo ~info ~body:c ~uctx ~obl_hook ~opaque:false obls in - pm + Declare.Obls.add_definition ~pm:st ~cinfo ~info ~body:c ~uctx ~obl_hook ~opaque:false obls | TmQuote trm -> (* user should do the reduction (using tmEval) if they want *)