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 /engine/evd.mli | |
| 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 'engine/evd.mli')
| -rw-r--r-- | engine/evd.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index 29235050b0..3cb4031f11 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -495,7 +495,7 @@ val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t option contained in the object; need the term to be evar-normal otherwise defined evars are returned too. *) -val evars_of_term : constr -> Evar.Set.t +val evars_of_term : econstr -> Evar.Set.t (** including evars in instances of evars *) val evars_of_named_context : (econstr, etypes) Context.Named.pt -> Evar.Set.t |