From 055981b13cb4222632a46dbdf07859f522569d52 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 7 Jun 2005 15:44:16 +0000 Subject: [PATCH] added whd to match argument in guarded_by_destructors; before only verbatim occurrences of safe variables were accepted. --- helm/ocaml/cic_proof_checking/cicTypeChecker.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 9f5b280af..fbcf25f91 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -903,7 +903,7 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes = (fun (_,t) i -> i && guarded_by_destructors context n nn kl x safes t) exp_named_subst true | C.MutCase (uri,i,outtype,term,pl) -> - (match term with + (match CicReduction.whd context term with C.Rel m when List.mem m safes || m = x -> let (tys,len,isinductive,paramsno,cl) = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in -- 2.39.2