diff options
| author | Pierre-Marie Pédrot | 2019-05-14 23:28:11 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-14 23:28:11 +0200 |
| commit | 2fa28cedc140580fcf4231f7270b68b24e3c1230 (patch) | |
| tree | 12db4bb4cf331376faa84244b47b2cd5887aba3a /engine/proofview.ml | |
| parent | 2a60906dd9d295615bcfa4b1fce8cea9626d965f (diff) | |
| parent | ce083774403b70d58c71c5a6ba104c337613add4 (diff) | |
Merge PR #8893: Moving evars_of_term from constr to econstr
Ack-by: SkySkimmer
Reviewed-by: gares
Ack-by: herbelin
Reviewed-by: maximedenes
Reviewed-by: ppedrot
Diffstat (limited to 'engine/proofview.ml')
| -rw-r--r-- | engine/proofview.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index ecea637947..1fd8b5d50e 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -641,7 +641,7 @@ let shelve_goals l = [sigma]. *) let depends_on sigma src tgt = let evi = Evd.find sigma tgt in - Evar.Set.mem src (Evd.evars_of_filtered_evar_info (Evarutil.nf_evar_info sigma evi)) + Evar.Set.mem src (Evd.evars_of_filtered_evar_info sigma (Evarutil.nf_evar_info sigma evi)) let unifiable_delayed g l = CList.exists (fun (tgt, lazy evs) -> not (Evar.equal g tgt) && Evar.Set.mem g evs) l @@ -1251,9 +1251,9 @@ module V82 = struct let goals = CList.map (fun (t,_) -> fst (Constr.destEvar (EConstr.Unsafe.to_constr t))) initial in { Evd.it = goals ; sigma=solution; } - let top_evars initial = + let top_evars initial { solution=sigma; } = let evars_of_initial (c,_) = - Evar.Set.elements (Evd.evars_of_term (EConstr.Unsafe.to_constr c)) + Evar.Set.elements (Evd.evars_of_term sigma c) in CList.flatten (CList.map evars_of_initial initial) |