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/evd.mli | |
| 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/evd.mli')
| -rw-r--r-- | engine/evd.mli | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index 29235050b0..587a1de044 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -491,16 +491,15 @@ val extract_changed_conv_pbs : evar_map -> val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t option -(** The following functions return the set of evars immediately - contained in the object; need the term to be evar-normal otherwise - defined evars are returned too. *) +(** The following functions return the set of undefined evars + contained in the object. *) -val evars_of_term : constr -> Evar.Set.t +val evars_of_term : evar_map -> econstr -> Evar.Set.t (** including evars in instances of evars *) -val evars_of_named_context : (econstr, etypes) Context.Named.pt -> Evar.Set.t +val evars_of_named_context : evar_map -> (econstr, etypes) Context.Named.pt -> Evar.Set.t -val evars_of_filtered_evar_info : evar_info -> Evar.Set.t +val evars_of_filtered_evar_info : evar_map -> evar_info -> Evar.Set.t (** Metas *) val meta_list : evar_map -> (metavariable * clbinding) list |