aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
authorHugo Herbelin2018-10-09 19:58:17 +0200
committerHugo Herbelin2018-10-14 13:27:34 +0200
commitfcf027f0caf42b9133b50bb6cb76c16087975f33 (patch)
treef20129426483f92216f9da06181188796e38dd47 /engine
parent405a80db00537b5ccfb3b8655cd7baf61e890b20 (diff)
Removing useless call to Global.env in check_and_clear_in_constr.
Diffstat (limited to 'engine')
-rw-r--r--engine/evarutil.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index fc2189f870..13356627f0 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -579,7 +579,7 @@ let rec check_and_clear_in_constr env evdref err ids global c =
has dependencies in another hyp of the context of ev
and transitively remember the dependency *)
let check id _ =
- if occur_var_in_decl (Global.env ()) !evdref id h
+ if occur_var_in_decl env !evdref id h
then raise (Depends id)
in
let () = Id.Map.iter check ri in