diff options
| author | Hugo Herbelin | 2014-10-12 15:32:38 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-13 19:12:34 +0200 |
| commit | 267d7a63e9c24573226d0890bedb783f10dcb235 (patch) | |
| tree | 9086f77abd7a96d89d9b9e9272ac4aa87f256223 /pretyping | |
| parent | 9632987e1eb0b035c760ab293e785c752d5eac92 (diff) | |
Adding a tactic which fails if one of the goals under focus is dependent in another one.
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 |