X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fwhelp%2FfwdQueries.ml;h=5387d3aeb170f21b866b778e0dc3d997fc7e8285;hb=0d9db17cef4232805de6193f5ff0028a3c99d908;hp=1f4e508fc032f7534d82e32b44a706b6a199ccac;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/whelp/fwdQueries.ml b/components/whelp/fwdQueries.ml
index 1f4e508fc..5387d3aeb 100644
--- a/components/whelp/fwdQueries.ml
+++ b/components/whelp/fwdQueries.ml
@@ -104,7 +104,8 @@ let decomposables ~dbd =
       | None     -> None
       | Some str ->
          match CicUtil.term_of_uri (UriManager.uri_of_string str) with
-            | Cic.MutInd (uri, typeno, _) -> Some (uri, typeno)
+            | Cic.MutInd (uri, typeno, _) -> Some (uri, Some typeno)
+	    | Cic.Const (uri, _)          -> Some (uri, None)
 	    | _                           -> 
 	       raise (UriManager.IllFormedUri str)
    in
@@ -112,4 +113,3 @@ let decomposables ~dbd =
    let query = Printf.sprintf "SELECT %s FROM %s" select from in
    let decomposables = HMysql.map ~f:map (HMysql.exec dbd query) in
    filter_map_n (fun _ x -> x) 0 decomposables   
-