more proof irrelevance

[helm.git] / helm / software / components / ng_kernel / oCic2NCic.ml

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 56159ffa4e91846f28785b5af4c2b5667cec0d68..0ead3ff2f278bc430504791e9d26838ffdd230eb 100644 (file)
--- 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 *)