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 /plugins/ssr | |
| 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 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrview.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 075ebf006a..57a068f82a 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -290,7 +290,7 @@ let finalize_view s0 ?(simple_types=true) p = Goal.enter_one ~__LOC__ begin fun g -> let env = Goal.env g in let sigma = Goal.sigma g in - let evars_of_p = Evd.evars_of_term (EConstr.to_constr ~abort_on_undefined_evars:false sigma p) in + let evars_of_p = Evd.evars_of_term p in let filter x _ = Evar.Set.mem x evars_of_p in let sigma = Typeclasses.resolve_typeclasses ~fail:false ~filter env sigma in let p = Reductionops.nf_evar sigma p in |