Modified filtering function

[helm.git] / helm / ocaml / tactics / newConstraints.ml

diff --git a/helm/ocaml/tactics/newConstraints.ml b/helm/ocaml/tactics/newConstraints.ml
index 00cf279568d7bec0acfd0c60b0e856d3b308a30f..f384e6f4de9c8ba24456a078439373d24be8c5e1 100644 (file)
--- a/helm/ocaml/tactics/newConstraints.ml
+++ b/helm/ocaml/tactics/newConstraints.ml
@@ -310,3 +310,11 @@ let prefixes n t =
     | None, set when (SetSet.is_empty set) -> None, []
     | _, _ -> assert false
 ;;
+
+let mainandcons t =
+  let const = constants_concl t in
+  match prefixes 1 t with 
+    Some main, _ -> main, const
+  | _,_ ->  assert false
+;;
+