]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/mQueryLevels2.mli
Minor widget rearrangement.
[helm.git] / helm / gTopLevel / mQueryLevels2.mli
index 822564d3ae3d8f295f2bb4e7d8ffcec15e8c820b..805f1064da2517efbe5a5a962f1ef7cf2844f614 100644 (file)
 (*                                                                            *)
 (******************************************************************************)
 
-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)
+val get_constraints: Cic.term -> MQueryGenerator.must_restrictions