From 01dd8b3dcbf02a9645152496d64f649afbbd22b9 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 27 Aug 2012 12:02:53 +0000 Subject: [PATCH] No pattern matching over empty types in Haskell --- matita/components/ng_kernel/nCicExtraction.ml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/matita/components/ng_kernel/nCicExtraction.ml b/matita/components/ng_kernel/nCicExtraction.ml index 691d8143d..32f5bc35e 100644 --- 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 -- 2.39.2