1. The depth constraint on Rels and Sorts is now optional.

[helm.git] / helm / gTopLevel / mQueryLevels2.mli

diff --git a/helm/gTopLevel/mQueryLevels2.mli b/helm/gTopLevel/mQueryLevels2.mli
index 822564d3ae3d8f295f2bb4e7d8ffcec15e8c820b..584ec6909477d66af4a9a15db547725ac461a900 100644 (file)
--- a/helm/gTopLevel/mQueryLevels2.mli
+++ b/helm/gTopLevel/mQueryLevels2.mli
@@ -35,10 +35,4 @@
 
 val get_constraints:
  Cic.term ->
-(*
-  MQueryGenerator.must_restrictions * MQueryGenerator.can_restrictions
-*)
- ((string * string * int option) list * (string * int) list *
-  (string * int * string) list) *
- ((string * string * int option) list option * (string * int) list option *
-  (string * int * string) list option)
+  MQueryGenerator.must_restrictions * MQueryGenerator.only_restrictions