X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FoCic2NCic.ml;fp=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FoCic2NCic.ml;h=0ead3ff2f278bc430504791e9d26838ffdd230eb;hb=a3b43762ca9cfb746933dcd991bfc363b5fdd9b7;hp=56159ffa4e91846f28785b5af4c2b5667cec0d68;hpb=3cd093c8c3f5454514802e5d3ae5edc150dbbf72;p=helm.git

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 56159ffa4..0ead3ff2f 100644
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -46,10 +46,12 @@ let get_relevance ty =
   match CicReduction.whd context ty with
       Cic.Prod (n,s,t) ->
         not (is_proof_irrelevant context s)::aux (Some (n,Cic.Decl s)::context) t
-    | ty -> if is_proof_irrelevant context ty then raise InProp else []
+    | _ -> []
+ in aux [] ty
+(*    | ty -> if is_proof_irrelevant context ty then raise InProp else []
  in
    try aux [] ty
-   with InProp -> []
+   with InProp -> []*)
 ;;
 
 (* porcatissima *)