X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FnewConstraints.ml;h=f384e6f4de9c8ba24456a078439373d24be8c5e1;hb=3bb4ce11fb9d4c6375483a80344beb94c4517dd7;hp=00cf279568d7bec0acfd0c60b0e856d3b308a30f;hpb=90a88a05bb66c0e14a95d54929a4b545c8f2a36c;p=helm.git

diff --git a/helm/ocaml/tactics/newConstraints.ml b/helm/ocaml/tactics/newConstraints.ml
index 00cf27956..f384e6f4d 100644
--- 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
+;;
+