X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FoCic2NCic.ml;h=0ead3ff2f278bc430504791e9d26838ffdd230eb;hb=6033870314160f36fa814914550682b304beaba0;hp=56159ffa4e91846f28785b5af4c2b5667cec0d68;hpb=28f01bb2d0e5f1b3f180b0b478267d2beb06a5fe;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 *)