Exporting apply_subfilter from Evd.ml.

2 files changed, 16 insertions, 9 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index a1f84622a9..aa2ca0009b 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -28,6 +28,7 @@ sig
   val filter_array : t -> 'a array -> 'a array
   val extend : int -> t -> t
   val compose : t -> t -> t
+  val apply_subfilter : t -> bool list -> t
   val restrict_upon : t -> int -> (int -> bool) -> t option
   val map_along : (bool -> 'a -> bool) -> t -> 'a list -> t
   val make : bool list -> t
@@ -81,7 +82,12 @@ struct
     | None -> None
     | Some f2 -> normalize (CList.filter_with f1 f2)
 
-  let apply_subfilter filter subfilter =
+  let apply_subfilter_array filter subfilter =
+    (** In both cases we statically know that the argument will contain at
+        least one [false] *)
+    match filter with
+    | None -> Some (Array.to_list subfilter)
+    | Some f ->
     let len = Array.length subfilter in
     let fold b (i, ans) =
       if b then
@@ -90,19 +96,16 @@ struct
       else
         (i, false :: ans)
     in
-    snd (List.fold_right fold filter (pred len, []))
+    Some (snd (List.fold_right fold f (pred len, [])))
+
+  let apply_subfilter filter subfilter =
+    apply_subfilter_array filter (Array.of_list subfilter)
 
   let restrict_upon f len p =
     let newfilter = Array.init len p in
     if Array.for_all (fun id -> id) newfilter then None
     else
-      (** In both cases we statically know that the argument will contain at
-          least one [false] *)
-      let nf = match f with
-      | None -> Some (Array.to_list newfilter)
-      | Some f -> Some (apply_subfilter f newfilter)
-      in
-      Some nf
+      Some (apply_subfilter_array f newfilter)
 
   let map_along f flt l =
     let ans = match flt with
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index be8ca7cd51..bbae32d8ca 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -58,6 +58,10 @@ sig
   (** Horizontal composition : [compose f1 f2] only keeps parts of [f2] where
       [f1] is set. In particular, [f1] and [f2] must have the same length. *)
 
+  val apply_subfilter : t -> bool list -> t
+  (** [apply_subfilter f1 f2] applies filter [f2] where [f1] is [true]. In
+      particular, the length of [f2] is the number of times [f1] is [true] *)
+
   val restrict_upon : t -> int -> (int -> bool) -> t option
   (** Ad-hoc primitive. *)