X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FmQueryLevels2.ml;h=afd0ee42b957c4bb6311003c35e2185cdb5fc09c;hb=9f694d4bf47c7772dda4827f1b46f42cb435ec36;hp=80bbdf1b62682caed44567599f4809a4f8af8836;hpb=a370bf72d9e59254327ae3801ed4201f9981c6f0;p=helm.git

diff --git a/helm/gTopLevel/mQueryLevels2.ml b/helm/gTopLevel/mQueryLevels2.ml
index 80bbdf1b6..afd0ee42b 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 _
@@ -88,7 +88,7 @@ let get_constraints term =
             let s' =
              match s with
                 Cic.Prop ->
-                 "http://www.cs.unibo.it/helm/schemas/schema-helm#Prod"
+                 "http://www.cs.unibo.it/helm/schemas/schema-helm#Prop"
               | Cic.Set ->
                  "http://www.cs.unibo.it/helm/schemas/schema-helm#Set"
               | Cic.Type ->
@@ -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
 ;;