diff options
Diffstat (limited to 'vernac/declareDef.ml')
| -rw-r--r-- | vernac/declareDef.ml | 2 |
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; |