From 08791e80816548121e81e04d3ead8c9a5171d033 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 11 Jul 2005 11:04:14 +0000 Subject: [PATCH] Bug fixed in check_sort_elimination in the case (not tested so far) dummy = false, Prop vs Type. --- .../cic_proof_checking/cicTypeChecker.ml | 28 +++++++++---------- 1 file changed, 13 insertions(+), 15 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 1db82a99f..43805cf8b 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -1299,21 +1299,19 @@ and check_allowed_sort_elimination ~logger context uri i need_dummy ind false,ugraph1 else (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with - C.Sort C.Prop -> true,ugraph1 - | (C.Sort C.Set | C.Sort C.CProp) -> - (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with - C.InductiveDefinition (itl,_,_,_) -> - let (_,_,_,cl) = List.nth itl i in - (* is a singleton definition? *) - List.length cl = 1,ugraph1 - | _ -> - raise (TypeCheckerFailure - ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri)) - ) - | _ -> false,ugraph1 - ) + C.Sort C.Prop -> true,ugraph1 + | (C.Sort C.Set | C.Sort C.CProp | C.Sort (C.Type _)) -> + (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + match o with + C.InductiveDefinition (itl,_,_,_) -> + let (_,_,_,cl) = List.nth itl i in + (* is a singleton definition or the empty proposition? *) + (List.length cl = 1 || List.length cl = 0),ugraph1 + | _ -> + raise (TypeCheckerFailure + ("Unknown mutual inductive definition:" ^ + UriManager.string_of_uri uri))) + | _ -> false,ugraph1) | ((C.Sort C.Set, C.Prod (name,so,ta)) | (C.Sort C.CProp, C.Prod (name,so,ta))) when not need_dummy -> -- 2.39.2