aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/comDefinition.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-05-03 17:44:34 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-05-25 14:55:49 +0200
commitdfaf7e1ca5aebfdfbef5f32d235a948335f7fda0 (patch)
tree33fdd7c2eb44e54e7777e2d074127b129c5385ac /vernac/comDefinition.ml
parentd2533da244f770261478ae829167cb3a8ad38038 (diff)
Remove some occurrences of Evd.empty
We address the easy ones, but they should probably be all removed.
Diffstat (limited to 'vernac/comDefinition.ml')
-rw-r--r--vernac/comDefinition.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 863adb0d1..2d4bd6779 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -104,7 +104,9 @@ let interp_definition pl bl poly red_option c ctypopt =
(red_constant_entry (Context.Rel.length ctx) ce evd red_option, evd, decl, imps)
let check_definition (ce, evd, _, imps) =
- check_evars_are_solved (Global.env ()) evd Evd.empty;
+ let env = Global.env () in
+ let empty_sigma = Evd.from_env env in
+ check_evars_are_solved env evd empty_sigma;
ce
let do_definition ~program_mode ident k univdecl bl red_option c ctypopt hook =