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

2. "only" (ex "can") constraints are copies of the "must" constraints

diff --git a/helm/gTopLevel/mQueryLevels2.ml b/helm/gTopLevel/mQueryLevels2.ml
index c4bf895ddfeb91182bcca20c7d09f19615da82ea..afd0ee42b957c4bb6311003c35e2185cdb5fc09c 100644 (file)
--- a/helm/gTopLevel/mQueryLevels2.ml
+++ b/helm/gTopLevel/mQueryLevels2.ml
@@ -80,7 +80,7 @@ let get_constraints term =
        let kind',depth = !!kind in
         (match depth with
             None -> [],[],[]
-          | Some d -> [],[kind',d],[])
+          | Some d -> [],[kind',Some d],[])
     | C.Sort s ->
        (match kind with
            Backbone _
@@ -97,7 +97,7 @@ let get_constraints term =
              let kind',depth = !!kind in
               (match depth with
                   None -> assert false
-                | Some d -> [],[],[kind',d,s'])
+                | Some d -> [],[],[kind',Some d,s'])
          | _ -> [],[],[])
     | C.Meta _
     | C.Implicit -> assert false
@@ -166,8 +166,11 @@ let get_constraints term =
    (fun i (_,t) -> i @@ (process_type_aux (soften_classification kind) t))
    ([],[],[])
 in
- process_type_aux (Backbone 0) (CicMiniReduction.letin_nf term),
-  (None,None,None)
+ let obj_constraints,rel_constraints,sort_constraints =
+  process_type_aux (Backbone 0) (CicMiniReduction.letin_nf term)
+ in
+  (obj_constraints,rel_constraints,sort_constraints),
+   (Some obj_constraints,Some rel_constraints,Some sort_constraints)
 ;;
 
 (*CSC: Debugging only *)
@@ -184,10 +187,16 @@ let get_constraints term =
   prerr_endline "Constraints on Rels:" ;
   List.iter
    (function (s,n) ->
-     prerr_endline (s ^ " " ^ string_of_int n)) rels ;
+     prerr_endline
+      (s ^ " " ^ (match n with Some n' -> string_of_int n' | None -> "NULL"))
+   ) rels ;
   prerr_endline "Constraints on Sorts:" ;
   List.iter
    (function (s1,n,s2) ->
-     prerr_endline (s1 ^ " " ^ string_of_int n ^ " " ^ s2)) sorts ;
+     prerr_endline
+      (s1 ^ " " ^ (match n with Some n' -> string_of_int n' | None -> "NULL") ^
+        " " ^ s2)
+   ) sorts ;
+  prerr_endline "The \"only\" constraints are the same." ;
   res
 ;;

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