diff options
Diffstat (limited to 'vernac/comDefinition.ml')
| -rw-r--r-- | vernac/comDefinition.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 472411ac3a..9c80f1d2f5 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -87,8 +87,7 @@ let interp_definition pl bl poly red_option c ctypopt = let check_definition (ce, evd, _, imps) = let env = Global.env () in - let empty_sigma = Evd.from_env env in - check_evars_are_solved env evd empty_sigma; + check_evars_are_solved env evd; ce let do_definition ~program_mode ident k univdecl bl red_option c ctypopt hook = |