Appl case in is_really_smaller fixed as in the old kernel

[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..9336cb84ab3c6e8af65624525867ee6f1b9035fc 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -763,10 +763,12 @@ and check_is_really_smaller_arg
  match CicReduction.whd ~subst context te with
      C.Rel m when List.mem m safes -> true
    | C.Rel _ 
-   | C.Appl _
    | C.MutConstruct _
    | C.Const _
    | C.Var _ -> false
+   | C.Appl (he::_) ->
+        check_is_really_smaller_arg rec_uri rec_uri_len 
+          ~logger ~metasenv ~subst context n nn kl x safes he
    | C.Lambda (name,ty,ta) ->
       check_is_really_smaller_arg rec_uri rec_uri_len 
         ~logger ~metasenv ~subst (Some (name,Cic.Decl ty)::context)
@@ -1781,20 +1783,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}