Adapt to PR #18795

MetaCoq · May 20, 2024 · 9a28be1 · 9a28be1
1 parent e27b549
commit 9a28be1
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/template-coq/src/plugin_core.ml b/template-coq/src/plugin_core.ml
@@ -131,7 +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 ~term:c ~uctx:ctx ~obl_hook obls in
+    let pm, _ = Declare.Obls.add_definition ~pm:st ~cinfo ~info ~body:c ~uctx:ctx ~obl_hook ~opaque:false obls in
     pm
 
 let tmFreshName (nm : ident) : ident tm =

diff --git a/template-coq/src/run_template_monad.ml b/template-coq/src/run_template_monad.ml
@@ -436,7 +436,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 ~term:c ~uctx ~obl_hook obls in
+    let pm, _ = Declare.Obls.add_definition ~pm:st ~cinfo ~info ~body:c ~uctx ~obl_hook ~opaque:false obls in
     pm
 
   | TmQuote trm ->