aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/logic.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml
index d664013c72..4c6e5bacfa 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -70,9 +70,9 @@ let with_check = Options.with_option check
(instead of iterating on the list of identifier to be removed, which
forces the user to give them in order). *)
let clear_hyps sigma ids gl =
- let evd = ref (Evd.create_goal_evar_defs sigma) in
- let ngl = Evarutil.clear_hyps_in_evi evd gl ids in
- (ngl, evars_of !evd)
+ let evdref = ref (Evd.create_goal_evar_defs sigma) in
+ let ngl = Evarutil.clear_hyps_in_evi evdref gl ids in
+ (ngl, evars_of !evdref)
(* The ClearBody tactic *)