diff options
Diffstat (limited to 'pretyping/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index cf788f36d9..1f944587ea 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -605,6 +605,13 @@ let extract_all_conv_pbs evd = let evar_merge evd evars = { evd with evars = EvarMap.merge evd.evars evars.evars } +let evar_list evd c = + let rec evrec acc c = + match kind_of_term c with + | Evar (evk, _ as ev) when mem evd evk -> ev :: acc + | _ -> fold_constr evrec acc c in + evrec [] c + (**********************************************************) (* Sort variables *) |