diff --git a/template-coq/src/plugin_core.ml b/template-coq/src/plugin_core.ml
index ef58feaa7..836e876fa 100644
--- 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
index 3f69708a9..31c18e127 100644
--- 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 ->