Merge PR #9410: Make `Program` a regular attribute

Ack-by: SkySkimmer
Reviewed-by: aspiwack
Reviewed-by: ejgallego
Reviewed-by: gares
Reviewed-by: mattam82
Ack-by: maximedenes

1 files changed, 1 insertions, 1 deletions

diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 41057f8ab2..361ed1a737 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -57,7 +57,7 @@ let declare_fix ?(opaque = false) (_,poly,_ as kind) pl univs f ((def,_),eff) t
 
 let check_definition_evars ~allow_evars sigma =
   let env = Global.env () in
-  if not allow_evars then Pretyping.check_evars_are_solved env sigma
+  if not allow_evars then Pretyping.check_evars_are_solved ~program_mode:false env sigma
 
 let prepare_definition ~allow_evars ?opaque ?inline ~poly sigma udecl ~types ~body =
   check_definition_evars ~allow_evars sigma;