diff options
| author | ppedrot | 2013-10-27 15:02:43 +0000 |
|---|---|---|
| committer | ppedrot | 2013-10-27 15:02:43 +0000 |
| commit | 4c2302a2db3da1095ce9167ad0e4956defd3947f (patch) | |
| tree | f528bcab8e1d39b741cd3b88df74733e37f78c09 /proofs | |
| parent | d28285fa1c05297c7618a887b1758e283a9ebe64 (diff) | |
Abstracting evar filter away. The API is not perfect, but better than nothing.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16939 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/goal.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index 7901ec0a57..bb9128e1d3 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -494,8 +494,8 @@ module V82 = struct let mk_goal evars hyps concl extra = let evi = { Evd.evar_hyps = hyps; Evd.evar_concl = concl; - Evd.evar_filter = List.map (fun _ -> true) - (Environ.named_context_of_val hyps); + Evd.evar_filter = Evd.Filter.identity + (List.length (Environ.named_context_of_val hyps)); Evd.evar_body = Evd.Evar_empty; Evd.evar_source = (Loc.ghost,Evar_kinds.GoalEvar); Evd.evar_candidates = None; @@ -557,8 +557,8 @@ module V82 = struct let hyps = evi.Evd.evar_hyps in let new_hyps = List.fold_right Environ.push_named_context_val extra_hyps hyps in - let extra_filter = List.map (fun _ -> true) extra_hyps in - let new_filter = extra_filter @ evi.Evd.evar_filter in + let extra_filter = Evd.Filter.identity (List.length extra_hyps) in + let new_filter = Evd.Filter.append extra_filter evi.Evd.evar_filter in let new_evi = { evi with Evd.evar_hyps = new_hyps; Evd.evar_filter = new_filter } in let new_evi = Typeclasses.mark_unresolvable new_evi in |