diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evd.ml | 6 | ||||
| -rw-r--r-- | pretyping/evd.mli | 3 |
2 files changed, 9 insertions, 0 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 028361185e..f85970a1f8 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1572,6 +1572,12 @@ let evar_source_of_meta mv evd = | Anonymous -> (Loc.ghost,Evar_kinds.GoalEvar) | Name id -> (Loc.ghost,Evar_kinds.VarInstance id) +let dependent_evar_ident ev evd = + let evi = find evd ev in + match evi.evar_source with + | (_,Evar_kinds.VarInstance id) -> id + | _ -> anomaly (str "Not an evar resulting of a dependent binding") + (*******************************************************************) type open_constr = evar_map * constr diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 467e1a1636..542e2342f2 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -264,6 +264,9 @@ val rename : existential_key -> Id.t -> evar_map -> evar_map val evar_key : Id.t -> evar_map -> existential_key val evar_source_of_meta : metavariable -> evar_map -> Evar_kinds.t located + +val dependent_evar_ident : existential_key -> evar_map -> Id.t + (** {5 Side-effects} *) val emit_side_effects : Declareops.side_effects -> evar_map -> evar_map |