X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FmQueryLevels2.ml;h=968d2a35e8d6439c65c0549bc35d7f58c372f383;hb=370f967a478c116fcc85a81c7953363b4351a2e9;hp=c4bf895ddfeb91182bcca20c7d09f19615da82ea;hpb=4cbd4cadc2e71d4d25469dd7dddf05088baacb62;p=helm.git

diff --git a/helm/gTopLevel/mQueryLevels2.ml b/helm/gTopLevel/mQueryLevels2.ml
index c4bf895dd..968d2a35e 100644
--- 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,14 +166,16 @@ 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)
 ;;
 
 (*CSC: Debugging only *)
 let get_constraints term =
  let res = get_constraints term in
- let ((objs,rels,sorts),can) = res in
+ let (objs,rels,sorts) = res in
   prerr_endline "Constraints on objs:" ;
   List.iter
    (function (s1,s2,n) ->
@@ -184,10 +186,15 @@ 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 ;
   res
 ;;