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 | |
| 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')
| -rw-r--r-- | plugins/ssr/ssrview.ml | 2 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml | 4 |
2 files changed, 3 insertions, 3 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 diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 4e0866a0c5..e421b31227 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -544,7 +544,7 @@ let dont_impact_evars_in cl = (* - w_unify expands let-in (zeta conversion) eagerly, whereas we want to *) (* match a head let rigidly. *) let match_upats_FO upats env sigma0 ise orig_c = - let dont_impact_evars = dont_impact_evars_in orig_c in + let dont_impact_evars = dont_impact_evars_in (EConstr.of_constr orig_c) in let rec loop c = let f, a = splay_app ise c in let i0 = ref (-1) in let fpats = @@ -586,7 +586,7 @@ let match_upats_FO upats env sigma0 ise orig_c = let match_upats_HO ~on_instance upats env sigma0 ise c = - let dont_impact_evars = dont_impact_evars_in c in + let dont_impact_evars = dont_impact_evars_in (EConstr.of_constr c) in let it_did_match = ref false in let failed_because_of_TC = ref false in let rec aux upats env sigma0 ise c = |