diff options
| author | Pierre-Marie Pédrot | 2020-09-09 11:07:52 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-09 11:07:52 +0200 |
| commit | 6f12c3e3ccce7028abb492f804d30ba0bef58f06 (patch) | |
| tree | db89fb070eead9bcf14880a9b3d3672b0f5bbf85 /engine/evd.mli | |
| parent | 215d3013312309d47dae01b66b1781b572d30783 (diff) | |
| parent | fbe0ea439ed3cf2ad933bd6094a36b5cebc5bd19 (diff) | |
Merge PR #7825: [tactics] Refine test for unresolved evars: not reachable from initial evars
Ack-by: JasonGross
Ack-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: jfehrle
Ack-by: maximedenes
Reviewed-by: ppedrot
Diffstat (limited to 'engine/evd.mli')
| -rw-r--r-- | engine/evd.mli | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index 9394f9a9dd..fafaad9a04 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -284,8 +284,11 @@ val restrict : Evar.t-> Filter.t -> ?candidates:econstr list -> possibly limiting the instances to a set of candidates (candidates are filtered according to the filter) *) -val is_restricted_evar : evar_map -> Evar.t -> Evar.t option -(** Tell if an evar comes from restriction of another evar, and if yes, which *) +val get_aliased_evars : evar_map -> Evar.t Evar.Map.t +(** The map of aliased evars *) + +val is_aliased_evar : evar_map -> Evar.t -> Evar.t option +(** Tell if an evar has been aliased to another evar, and if yes, which *) val set_typeclass_evars : evar_map -> Evar.Set.t -> evar_map (** Mark the given set of evars as available for resolution. @@ -388,7 +391,6 @@ val pop_future_goals : evar_map -> FutureGoals.t * evar_map val fold_future_goals : (evar_map -> Evar.t -> evar_map) -> evar_map -> evar_map - val remove_future_goal : evar_map -> Evar.t -> evar_map val pr_future_goals_stack : evar_map -> Pp.t |