diff options
| author | Hugo Herbelin | 2018-11-01 23:26:06 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-05-13 18:23:58 +0200 |
| commit | 6211fd6e067e781a160db8765dd87067428048f2 (patch) | |
| tree | fa36209357839891624f3c3a88a042e45485e41e /engine/proofview.ml | |
| parent | 9f11eeefc204bdad029b66f30bc6c52377af63ae (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.ml | 2 |
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) |
