X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FtopLevel%2FtopLevel.ml;h=78aceae26f52ecafd4d53e07055e688bcda95737;hb=373eaf73bebec626e031a4a534ddfdd4f1c1b474;hp=d53ea70eaf5096cb4a015266a0d58fa958bca7c9;hpb=86122a3ce11bdf45ecb93f8f7efaffa49bd31fa2;p=helm.git

diff --git a/helm/gTopLevel/topLevel/topLevel.ml b/helm/gTopLevel/topLevel/topLevel.ml
index d53ea70ea..78aceae26 100644
--- a/helm/gTopLevel/topLevel/topLevel.ml
+++ b/helm/gTopLevel/topLevel/topLevel.ml
@@ -39,10 +39,9 @@ let get_terms () =
 let pp_type_of uri = 
    let u = UriManager.uri_of_string uri in  
    let s = match (CicEnvironment.get_obj u) with
-      | Cic.Definition (_, _, ty, _) -> CicPp.ppterm ty
-      | Cic.Axiom (_, ty, _)         -> CicPp.ppterm ty
-      | Cic.Variable (_, _, ty)      -> CicPp.ppterm ty
-      | _                            -> "Current proof or inductive definition."      
+      | Cic.Constant (_, _, ty, _) -> CicPp.ppterm ty
+      | Cic.Variable (_, _, ty, _) -> CicPp.ppterm ty
+      | _                          -> "Current proof or inductive definition."      
 (*
       | Cic.CurrentProof (_,conjs,te,ty) ->
       | C.InductiveDefinition _ ->