added a missing whd

[helm.git] / helm / software / components / cic_proof_checking / cicTypeChecker.ml

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 7ced8f113aa3997e621ea68456bf5815fbaa362d..883bc329600be45d2decfbefc498860fe837d4f7 100644 (file)
--- 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}