Added variousTactic with Constructor, Left, Right, Exists, Reflexivity, Symmetry...

[helm.git] / helm / gTopLevel / topLevel / topLevel.ml

diff --git a/helm/gTopLevel/topLevel/topLevel.ml b/helm/gTopLevel/topLevel/topLevel.ml
index d53ea70eaf5096cb4a015266a0d58fa958bca7c9..78aceae26f52ecafd4d53e07055e688bcda95737 100644 (file)
--- 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 _ ->