From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 17 Apr 2008 16:34:44 +0000 (+0000)
Subject: added a missing whd
X-Git-Tag: make_still_working~5327
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5acff80c93b3e3df4a52ff8cb9596de46f7bd924;p=helm.git

added a missing whd
---

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}