No pattern matching over empty types in Haskell

diff --git a/matita/components/ng_kernel/nCicExtraction.ml b/matita/components/ng_kernel/nCicExtraction.ml
index 691d8143dfcf63617b85414040810d3ebb79d98a..32f5bc35e6fd28cfcf6a4318268cd922c3607d59 100644 (file)
--- a/matita/components/ng_kernel/nCicExtraction.ml
+++ b/matita/components/ng_kernel/nCicExtraction.ml
@@ -748,6 +748,9 @@ let rec pretty_print_term status ctxt =
     | LetIn (name,s,t) ->
       "let " ^ name ^ " = " ^ pretty_print_term status ctxt s ^ " in " ^ pretty_print_term status (name@::ctxt) t
     | Match (r,matched,pl) ->
+      if pl = [] then
+       "error \"Case analysis over empty type\""
+      else
       let constructors, leftno =
       let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys status r in
       let _,_,_,cl  = List.nth tys n in