aboutsummaryrefslogtreecommitdiff
path: root/engine/proofview.ml
diff options
context:
space:
mode:
authorHugo Herbelin2018-11-01 23:26:06 +0100
committerHugo Herbelin2019-05-13 18:23:58 +0200
commit6211fd6e067e781a160db8765dd87067428048f2 (patch)
treefa36209357839891624f3c3a88a042e45485e41e /engine/proofview.ml
parent9f11eeefc204bdad029b66f30bc6c52377af63ae (diff)
Moving Evd.evars_of_term from constr to econstr + consequences.
This impacts a lot of code, apparently in the good, removing several conversions back and forth constr.
Diffstat (limited to 'engine/proofview.ml')
-rw-r--r--engine/proofview.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml
index ecea637947..b77839c28e 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1253,7 +1253,7 @@ module V82 = struct
let top_evars initial =
let evars_of_initial (c,_) =
- Evar.Set.elements (Evd.evars_of_term (EConstr.Unsafe.to_constr c))
+ Evar.Set.elements (Evd.evars_of_term c)
in
CList.flatten (CList.map evars_of_initial initial)