Add the possibility of defining opaque terms with program.

1 files changed, 2 insertions, 2 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 9cb3bb8660..608747d0e4 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -746,8 +746,8 @@ let interp_fix_body env_rec evdref impls (_,ctx) fix ccl =
 
 let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
 
-let declare_fix (_,poly,_ as kind) ctx f ((def,_),eff) t imps =
-  let ce = definition_entry ~types:t ~poly ~univs:ctx ~eff def in
+let declare_fix ?(opaque = false) (_,poly,_ as kind) ctx f ((def,_),eff) t imps =
+  let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in
   declare_definition f kind ce imps (Lemmas.mk_hook (fun _ r -> r))
 
 let _ = Obligations.declare_fix_ref := declare_fix