From 4c2302a2db3da1095ce9167ad0e4956defd3947f Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Sun, 27 Oct 2013 15:02:43 +0000
Subject: 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
---
 proofs/goal.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'proofs')

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
-- 
cgit v1.2.3