From 1f911ae5768c21f0f30c74cbc9bedf537477e5f5 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 7 Dec 2001 15:34:41 +0000 Subject: [PATCH] Bug partially fixed: the branch of a case of type Prod can be not a Lambda. (e.g. a Rel, a MutConstruct, etc.) I have fixed only the two cases of a Rel and a MutConstruct. --- helm/ocaml/cic_proof_checking/cicTypeChecker.ml | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 1b1595100..5363c5e64 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -459,9 +459,17 @@ and get_new_safes p c rl safes n nn x = if b then 1::safes' else safes' in get_new_safes ta2 ta1 tl safes'' (n+1) (nn+1) (x+1) - | (C.MutInd _, e, []) -> (e,safes,n,nn,x) + | (C.Prod _, (C.MutConstruct _ as e), _) + | (C.Prod _, (C.Rel _ as e), _) + | (C.MutInd _, e, []) | (C.Appl _, e, []) -> (e,safes,n,nn,x) - | (_,_,_) -> raise (Impossible 7) + | (_,_,_) -> + (* CSC: If the next exception is raised, it just means that *) + (* CSC: the proof-assistant allows to use very strange things *) + (* CSC: as a branch of a case whose type is a Prod. In *) + (* CSC: particular, this means that a new (C.Prod, x,_) case *) + (* CSC: must be considered in this match. (e.g. x = MutCase) *) + raise (Impossible 7) and split_prods n te = let module C = Cic in -- 2.39.2