diff options
| author | Hugo Herbelin | 2018-11-02 00:17:47 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-05-13 18:23:58 +0200 |
| commit | 6608f64f001f8f1a50b2dc41fefdf63c0b84b270 (patch) | |
| tree | 8e320caff90f9fb0bf774ae038b5fb95df985150 /plugins/ssr | |
| parent | 6211fd6e067e781a160db8765dd87067428048f2 (diff) | |
Passing evar_map to evars_of_term rather than expecting the term to be evar-nf.
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrview.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 57a068f82a..0a5c85f4ab 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 p in + let evars_of_p = Evd.evars_of_term sigma 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 @@ -307,7 +307,7 @@ Goal.enter_one ~__LOC__ begin fun g -> let und0 = (* Unassigned evars in the initial goal *) let sigma0 = Tacmach.project s0 in let g0info = Evd.find sigma0 (Tacmach.sig_it s0) in - let g0 = Evd.evars_of_filtered_evar_info g0info in + let g0 = Evd.evars_of_filtered_evar_info sigma0 g0info in List.filter (fun k -> Evar.Set.mem k g0) (List.map fst (Evar.Map.bindings (Evd.undefined_map sigma0))) in let rigid = rigid_of und0 in |