From 5acff80c93b3e3df4a52ff8cb9596de46f7bd924 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 17 Apr 2008 16:34:44 +0000 Subject: [PATCH 1/1] added a missing whd --- .../cic_proof_checking/cicTypeChecker.ml | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index 7ced8f113..883bc3296 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -1781,20 +1781,25 @@ end; let (m, eaten, context') = eat_lambdas ~subst (types @ context) (x + 1) bo in - let rec_uri, rec_uri_len = + let rec_uri, rec_uri_len = + let he = match List.hd context' with - | Some (_,Cic.Decl (Cic.MutInd (uri,_,_))) - | Some (_,Cic.Decl (Cic.Appl (Cic.MutInd (uri,_,_)::_))) -> + Some (_,Cic.Decl he) -> he + | _ -> assert false + in + match CicReduction.whd ~subst (List.tl context') he with + | Cic.MutInd (uri,_,_) + | Cic.Appl (Cic.MutInd (uri,_,_)::_) -> uri, - (match - CicEnvironment.get_obj + (match + CicEnvironment.get_obj CicUniv.oblivion_ugraph uri with | Cic.InductiveDefinition (tl,_,_,_), _ -> List.length tl | _ -> assert false) | _ -> assert false - in + in (* let's control the guarded by destructors conditions D{f,k,x,M} -- 2.39.2