diff options
| author |  Stephane Glondu <steph@glondu.net> | 2013-05-08 17:47:10 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 17:47:10 +0200 |
| commit | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (patch) | |
| tree | 09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /pretyping/evd.ml | |
| parent | bf12eb93f3f6a6a824a10878878fadd59745aae0 (diff) | |
Imported Upstream version 8.4pl2dfsgupstream/8.4pl2dfsg
Diffstat (limited to 'pretyping/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 6d5c98ce..4d9eb897 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -67,9 +67,12 @@ let evar_hyps evi = evi.evar_hyps let evar_context evi = named_context_of_val evi.evar_hyps let evar_body evi = evi.evar_body let evar_filter evi = evi.evar_filter -let evar_unfiltered_env evi = Global.env_of_context evi.evar_hyps let evar_filtered_context evi = snd (list_filter2 (fun b c -> b) (evar_filter evi,evar_context evi)) +let evar_filtered_hyps evi = + List.fold_right push_named_context_val (evar_filtered_context evi) + empty_named_context_val +let evar_unfiltered_env evi = Global.env_of_context evi.evar_hyps let evar_env evi = List.fold_right push_named (evar_filtered_context evi) (reset_context (Global.env())) |