From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 17 Apr 2008 16:12:12 +0000 (+0000)
Subject: new calculation of recursive parameters in guarded by destructors:
X-Git-Tag: make_still_working~5328
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=97b18234921aec71a8b89ec2c1b058e12e5e043c;p=helm.git

new calculation of recursive parameters in guarded by destructors:

  inductive I : Type :=
  | K : list (pair Type I) -> I

  let rec f t on t : I -> bool :=
  match t with
  | k ((nat, x)::_) -> f x
  | k _ -> true

is now accepted. the arg of k used to be recursive but not the head of the list
(only its tail) since constructors types were not specialized on actual left
arguments (and the information that the type of the head contains I was lost).
---

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 68bbe416a..7ced8f113 100644
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -54,7 +54,7 @@ let rec split l n =
       raise (TypeCheckerFailure (lazy "Parameters number < left parameters number"))
 ;;
 
-let debrujin_constructor ?(cb=fun _ _ -> ()) uri number_of_types =
+let debrujin_constructor ?(cb=fun _ _ -> ()) ?(check_exp_named_subst=true) uri number_of_types context =
  let rec aux k t =
   let module C = Cic in
   let res =
@@ -83,7 +83,7 @@ let debrujin_constructor ?(cb=fun _ _ -> ()) uri number_of_types =
        in
         C.Const (uri,exp_named_subst')
     | C.MutInd (uri',tyno,exp_named_subst) when UriManager.eq uri uri' ->
-       if exp_named_subst != [] then
+       if check_exp_named_subst && exp_named_subst != [] then
         raise (TypeCheckerFailure
           (lazy ("non-empty explicit named substitution is applied to "^
            "a mutual inductive type which is being defined"))) ;
@@ -121,7 +121,7 @@ let debrujin_constructor ?(cb=fun _ _ -> ()) uri number_of_types =
    cb t res;
    res
  in
-  aux 0
+  aux (List.length context)
 ;;
 
 exception CicEnvironmentError;;
@@ -557,7 +557,7 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph =
 	let ugraph'' = 
           List.fold_left
             (fun ugraph (name,te) -> 
-              let debrujinedte = debrujin_constructor uri len te in
+              let debrujinedte = debrujin_constructor uri len [] te in
               let augmented_term =
 		List.fold_right
 		  (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i))
@@ -666,58 +666,45 @@ and type_of_mutual_inductive_constr ~logger uri i j ugraph =
 
 and recursive_args context n nn te =
  let module C = Cic in
-  match CicReduction.whd context te with
-     C.Rel _ -> []
-   | C.Var _
-   | C.Meta _
-   | C.Sort _
-   | C.Implicit _
-   | C.Cast _ (*CSC ??? *) ->
-      raise (AssertFailure (lazy "3")) (* due to type-checking *)
-   | C.Prod (name,so,de) ->
-      (not (does_not_occur context n nn so)) ::
-       (recursive_args ((Some (name,(C.Decl so)))::context) (n+1) (nn + 1) de)
-   | C.Lambda _
-   | C.LetIn _ ->
-      raise (AssertFailure (lazy "4")) (* due to type-checking *)
-   | C.Appl _ -> []
-   | C.Const _ -> raise (AssertFailure (lazy "5"))
-   | C.MutInd _
-   | C.MutConstruct _
-   | C.MutCase _
-   | C.Fix _
-   | C.CoFix _ -> raise (AssertFailure (lazy "6")) (* due to type-checking *)
+ match CicReduction.whd context te with
+    C.Rel _ 
+  | C.MutInd _ -> []
+  | C.Var _
+  | C.Meta _
+  | C.Sort _
+  | C.Implicit _
+  | C.Cast _ (*CSC ??? *) ->
+     raise (AssertFailure (lazy "3")) (* due to type-checking *)
+  | C.Prod (name,so,de) ->
+     (not (does_not_occur context n nn so)) ::
+      (recursive_args ((Some (name,(C.Decl so)))::context) (n+1) (nn + 1) de)
+  | C.Lambda _
+  | C.LetIn _ ->
+     raise (AssertFailure (lazy "4")) (* due to type-checking *)
+  | C.Appl _ -> []
+  | C.Const _ -> raise (AssertFailure (lazy "5"))
+  | C.MutConstruct _
+  | C.MutCase _
+  | C.Fix _
+  | C.CoFix _ -> raise (AssertFailure (lazy "6")) (* due to type-checking *)
 
-and get_new_safes ~subst context p c rl safes n nn x =
+and get_new_safes ~subst context p rl safes n nn x =
  let module C = Cic in
  let module U = UriManager in
  let module R = CicReduction in
-  match (R.whd ~subst context c, R.whd ~subst context p, rl) with
-     (C.Prod (_,so,ta1), C.Lambda (name,_,ta2), b::tl) ->
-       (* we are sure that the two sources are convertible because we *)
-       (* have just checked this. So let's go along ...               *)
-       let safes' =
-        List.map (fun x -> x + 1) safes
-       in
-        let safes'' =
-         if b then 1::safes' else safes'
-        in
-         get_new_safes ~subst ((Some (name,(C.Decl so)))::context)
-          ta2 ta1 tl safes'' (n+1) (nn+1) (x+1)
-   | (C.Prod _, (C.MutConstruct _ as e), _)
-   | (C.Prod _, (C.Rel _ as e), _)
-   | (C.MutInd _, e, [])
-   | (C.Appl _, e, []) -> (e,safes,n,nn,x,context)
-   | (c,p,l) ->
-      (* CSC: If the next exception is raised, it just means that   *)
-      (* CSC: the proof-assistant allows to use very strange things *)
-      (* CSC: as a branch of a case whose type is a Prod. In        *)
-      (* CSC: particular, this means that a new (C.Prod, x,_) case  *)
-      (* CSC: must be considered in this match. (e.g. x = MutCase)  *)
+  match R.whd ~subst context p, rl with
+   | C.Lambda (name,so,ta), b::tl ->
+       let safes = List.map (fun x -> x + 1) safes in
+       let safes = if b then 1::safes else safes in
+       get_new_safes ~subst ((Some (name,(C.Decl so)))::context)
+          ta tl safes (n+1) (nn+1) (x+1)
+   | C.MutConstruct _ as e, _
+   | (C.Rel _ as e), _
+   | e, [] -> (e,safes,n,nn,x,context)
+   | p,_::_ ->
       raise
        (AssertFailure (lazy
-         (Printf.sprintf "Get New Safes: c=%s ; p=%s"
-           (CicPp.ppterm c) (CicPp.ppterm p))))
+         (Printf.sprintf "Get New Safes: p=%s" (CicPp.ppterm p))))
 
 and split_prods ~subst context n te =
  let module C = Cic in
@@ -741,7 +728,34 @@ and eat_lambdas ~subst context n te =
    | (n, te) ->
        raise (AssertFailure (lazy (sprintf "9 (%d, %s)" n (CicPp.ppterm te))))
 
-and check_is_really_smaller_arg ~subst context n nn kl x safes te =
+and specialize_inductive_type ~logger ~subst ~metasenv context t = 
+  let ty,_= type_of_aux' ~logger ~subst metasenv context t CicUniv.oblivion_ugraph in
+  match CicReduction.whd ~subst context ty with
+  | Cic.MutInd (uri,_,exp) 
+  | Cic.Appl (Cic.MutInd (uri,_,exp) :: _) as ty ->
+      let args = match ty with Cic.Appl (_::tl) -> tl | _ -> [] in
+      let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
+      (match o with
+      | Cic.InductiveDefinition (tl,_,paramsno,_) ->
+          let left_args,_ = HExtlib.split_nth paramsno args in
+          List.map (fun (name, isind, arity, cl) ->
+            let arity = CicSubstitution.subst_vars exp arity in
+            let arity = instantiate_parameters left_args arity in
+            let cl =
+              List.map
+               (fun (id,ty) -> 
+                 let ty = CicSubstitution.subst_vars exp ty in
+                 id, instantiate_parameters left_args ty) 
+               cl 
+            in
+            name, isind, arity, cl)
+          tl
+      | _ -> assert false)
+  | _ -> assert false
+
+and check_is_really_smaller_arg 
+  ~logger ~metasenv ~subst rec_uri rec_uri_len context n nn kl x safes te 
+=
  let module C = Cic in
  let module U = UriManager in
  (*CSC: we could perform beta-iota(-zeta?) immediately, and
@@ -754,60 +768,45 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
    | C.Const _
    | C.Var _ -> false
    | C.Lambda (name,ty,ta) ->
-      check_is_really_smaller_arg ~subst (Some (name,Cic.Decl ty)::context)
-       (n+1) (nn+1) kl (x+1) (List.map (fun n -> n+1) safes) ta
+      check_is_really_smaller_arg rec_uri rec_uri_len 
+        ~logger ~metasenv ~subst (Some (name,Cic.Decl ty)::context)
+        (n+1) (nn+1) kl (x+1) (List.map (fun n -> n+1) safes) ta
    | C.MutCase (uri,i,outtype,term,pl) ->
       (match term with
-          C.Rel m | C.Appl ((C.Rel m)::_) when List.mem m safes || m = x ->
-           let (lefts_and_tys,len,isinductive,paramsno,cl) =
-            let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
-            match o with
-               C.InductiveDefinition (tl,_,paramsno,_) ->
-                let (_,isinductive,_,cl) = List.nth tl i in
-                 let tys =
-                  List.map (fun (n,_,ty,_) ->
-                   Some(Cic.Name n,(Cic.Decl ty))) tl
-                 in
-                  let cl' =
-                   List.map
-                    (fun (id,ty) ->
-                      (id, snd (split_prods ~subst tys paramsno ty))) cl in
-                  let lefts =
-                   match tl with
-                      [] -> assert false
-                    | (_,_,ty,_)::_ ->
-                       fst (split_prods ~subst [] paramsno ty)
-                  in
-                   (lefts@tys,List.length tl,isinductive,paramsno,cl')
-             | _ ->
-                raise (TypeCheckerFailure
-                  (lazy ("Unknown mutual inductive definition:" ^
-                  UriManager.string_of_uri uri)))
-           in
-            if not isinductive then
-              List.fold_right
-               (fun p i ->
-                 i && check_is_really_smaller_arg ~subst context n nn kl x safes p)
-               pl true
-            else
-              List.for_all2
-               (fun p (_,c) ->
-                 let rl' =
-                  let debrujinedte = debrujin_constructor uri len c in
-                   recursive_args lefts_and_tys paramsno 
-                     (len+paramsno) debrujinedte
-                 in
-                  let (e, safes',n',nn',x',context') =
-                   get_new_safes ~subst context p c rl' safes n nn x
-                  in
-                  check_is_really_smaller_arg 
-                    ~subst context' n' nn' kl x' safes' e
-               ) pl cl
+      | C.Rel m | C.Appl ((C.Rel m)::_) when List.mem m safes || m = x ->
+         let tys = 
+           specialize_inductive_type ~logger ~subst ~metasenv context term 
+         in
+         let tys_ctx = 
+           List.map (fun (name,_,ty,_) -> Some (Cic.Name name, Cic.Decl ty)) tys
+         in
+         let _,isinductive,_,cl = List.nth tys i in
+         if not isinductive then
+           List.for_all
+            (check_is_really_smaller_arg rec_uri rec_uri_len 
+              ~logger ~metasenv ~subst context n nn kl x safes)
+            pl
+         else
+           List.for_all2
+            (fun p (_,c) ->
+              let rec_params =
+               let c = 
+                 debrujin_constructor ~check_exp_named_subst:false
+                  rec_uri rec_uri_len context c in
+               let len_ctx = List.length context in
+               recursive_args (context@tys_ctx) len_ctx (len_ctx+rec_uri_len) c
+              in
+              let (e, safes',n',nn',x',context') =
+                get_new_safes ~subst context p rec_params safes n nn x
+              in
+               check_is_really_smaller_arg rec_uri rec_uri_len 
+                ~logger ~metasenv ~subst context' n' nn' kl x' safes' e
+            ) pl cl
         | _ ->
-          List.fold_right
-           (fun p i ->
-             i && check_is_really_smaller_arg ~subst context n nn kl x safes p
-           ) pl true
+          List.for_all
+           (check_is_really_smaller_arg 
+             rec_uri rec_uri_len ~logger ~metasenv ~subst 
+             context n nn kl x safes) pl
       )
    | C.Fix (_, fl) ->
       let len = List.length fl in
@@ -821,16 +820,19 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
               len+1)
 	  ) ([],0) fl
        and safes' = List.map (fun x -> x + len) safes in
-        List.fold_right
-         (fun (_,_,_,bo) i ->
-           i &&
-            check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl
+        List.for_all
+         (fun (_,_,_,bo) ->
+            check_is_really_smaller_arg 
+              rec_uri rec_uri_len ~logger ~metasenv ~subst 
+                (tys@context) n_plus_len nn_plus_len kl
              x_plus_len safes' bo
-         ) fl true
+         ) fl
    | t ->
       raise (AssertFailure (lazy ("An inhabitant of an inductive type in normal form cannot have this shape: " ^ CicPp.ppterm t)))
 
-and guarded_by_destructors ~subst context n nn kl x safes t =
+and guarded_by_destructors 
+  ~logger ~metasenv ~subst rec_uri rec_uri_len context n nn kl x safes t 
+=
  let module C = Cic in
  let module U = UriManager in
   match CicReduction.whd ~subst context t with
@@ -839,7 +841,7 @@ and guarded_by_destructors ~subst context n nn kl x safes t =
       (match List.nth context (m-1) with
           Some (_,C.Decl _) -> true
         | Some (_,C.Def (bo,_)) ->
-           guarded_by_destructors ~subst context n nn kl x safes
+           guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes
             (CicSubstitution.lift m bo)
         | None -> raise (TypeCheckerFailure (lazy "Reference to deleted hypothesis"))
       )
@@ -847,36 +849,36 @@ and guarded_by_destructors ~subst context n nn kl x safes t =
    | C.Sort _
    | C.Implicit _ -> true
    | C.Cast (te,ty) ->
-      guarded_by_destructors ~subst context n nn kl x safes te &&
-       guarded_by_destructors ~subst context n nn kl x safes ty
+      guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes te &&
+       guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes ty
    | C.Prod (name,so,ta) ->
-      guarded_by_destructors ~subst context n nn kl x safes so &&
-       guarded_by_destructors ~subst ((Some (name,(C.Decl so)))::context)
+      guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes so &&
+       guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst ((Some (name,(C.Decl so)))::context)
         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
    | C.Lambda (name,so,ta) ->
-      guarded_by_destructors ~subst context n nn kl x safes so &&
-       guarded_by_destructors ~subst ((Some (name,(C.Decl so)))::context)
+      guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes so &&
+       guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst ((Some (name,(C.Decl so)))::context)
         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
    | C.LetIn (name,so,ty,ta) ->
-      guarded_by_destructors ~subst context n nn kl x safes so &&
-       guarded_by_destructors ~subst context n nn kl x safes ty &&
-        guarded_by_destructors ~subst ((Some (name,(C.Def (so,ty))))::context)
+      guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes so &&
+       guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes ty &&
+        guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst ((Some (name,(C.Def (so,ty))))::context)
          (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
       let k = List.nth kl (m - n - 1) in
        if not (List.length tl > k) then false
        else
-        List.fold_right
-         (fun param i ->
-           i && guarded_by_destructors ~subst context n nn kl x safes param
-         ) tl true &&
-         check_is_really_smaller_arg ~subst context n nn kl x safes (List.nth tl k)
+        List.for_all
+         (guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes) tl &&
+        check_is_really_smaller_arg 
+          rec_uri rec_uri_len 
+          ~logger ~metasenv ~subst context n nn kl x safes (List.nth tl k)
    | C.Var (_,exp_named_subst)
    | C.Const (_,exp_named_subst)
    | C.MutInd (_,_,exp_named_subst)
    | C.MutConstruct (_,_,_,exp_named_subst) ->
       List.for_all
-       (fun (_,t) -> guarded_by_destructors ~subst context n nn kl x safes t)
+       (fun (_,t) -> guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes t)
        exp_named_subst 
    | C.MutCase (uri,i,outtype,term,pl) ->
       (match CicReduction.whd ~subst context term with
@@ -884,59 +886,44 @@ and guarded_by_destructors ~subst context n nn kl x safes t =
         | C.Appl ((C.Rel m)::_) as t when List.mem m safes || m = x ->
            let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in
            List.for_all
-             (guarded_by_destructors ~subst context n nn kl x safes)
+             (guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes)
              tl &&
-           let (lefts_and_tys,len,isinductive,paramsno,cl) =
-	    let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
-            match o with
-               C.InductiveDefinition (tl,_,paramsno,_) ->
-                let (_,isinductive,_,cl) = List.nth tl i in
-                 let tys =
-                  List.map
-                   (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
-                 in
-                  let cl' =
-                   List.map
-                    (fun (id,ty) ->
-                      (id, snd (split_prods ~subst tys paramsno ty))) cl in
-                  let lefts =
-                   match tl with
-                      [] -> assert false
-                    | (_,_,ty,_)::_ ->
-                       fst (split_prods ~subst [] paramsno ty)
-                  in
-                   (lefts@tys,List.length tl,isinductive,paramsno,cl')
-             | _ ->
-                raise (TypeCheckerFailure
-                  (lazy ("Unknown mutual inductive definition:" ^
-                  UriManager.string_of_uri uri)))
+           let tys = 
+             specialize_inductive_type ~logger ~subst ~metasenv context t
+           in
+           let tys_ctx = 
+             List.map 
+               (fun (name,_,ty,_) -> Some (Cic.Name name, Cic.Decl ty)) tys
            in
+           let _,isinductive,_,cl = List.nth tys i in
             if not isinductive then
-             guarded_by_destructors ~subst context n nn kl x safes outtype &&
-              guarded_by_destructors ~subst context n nn kl x safes term &&
+             guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes outtype &&
+              guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes term &&
               List.for_all
-               (guarded_by_destructors ~subst context n nn kl x safes)
+               (guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes)
                pl
             else
-             guarded_by_destructors ~subst context n nn kl x safes outtype &&
+             guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes outtype &&
              List.for_all2
-               (fun p (_,c) ->
-                 let rl' =
-                  let debrujinedte = debrujin_constructor uri len c in
-                   recursive_args lefts_and_tys paramsno 
-                     (len+paramsno) debrujinedte
-                 in
-                  let (e, safes',n',nn',x',context') =
-                   get_new_safes ~subst context p c rl' safes n nn x
-                  in
-                   guarded_by_destructors ~subst context' n' nn' kl x' safes' e
+              (fun p (_,c) ->
+               let rec_params =
+                let c = 
+                 debrujin_constructor ~check_exp_named_subst:false 
+                  rec_uri rec_uri_len context c in
+                let len_ctx = List.length context in
+                recursive_args (context@tys_ctx) len_ctx (len_ctx+rec_uri_len) c
+               in
+               let (e, safes',n',nn',x',context') =
+                get_new_safes ~subst context p rec_params safes n nn x
+               in
+                guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context' n' nn' kl x' safes' e
                ) pl cl
         | _ ->
-          guarded_by_destructors ~subst context n nn kl x safes outtype &&
-           guarded_by_destructors ~subst context n nn kl x safes term &&
+          guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes outtype &&
+           guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes term &&
            (*CSC: manca ??? il controllo sul tipo di term? *)
            List.fold_right
-            (fun p i -> i && guarded_by_destructors ~subst context n nn kl x safes p)
+            (fun p i -> i && guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes p)
             pl true
       )
    | C.Appl (C.Fix (fixno, fl)::_) | C.Fix (fixno,fl) as t->
@@ -953,29 +940,30 @@ and guarded_by_destructors ~subst context n nn kl x safes t =
 	  ) ([],0) fl in
        let safes' = List.map (fun x -> x + len) safes in
         List.for_all
-         (guarded_by_destructors ~subst context n nn kl x safes) l &&
+         (guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes) l &&
         snd (List.fold_left
          (fun (fixno',i) (_,recno,ty,bo) ->
            fixno'+1,
            i &&
-           guarded_by_destructors ~subst context n nn kl x_plus_len safes' ty &&
+           guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x_plus_len safes' ty &&
            if
             fixno' = fixno &&
             List.length l > recno &&
             (*case where the recursive argument is already really_smaller *)
-            check_is_really_smaller_arg ~subst context n nn kl x safes
-             (List.nth l recno)
+            check_is_really_smaller_arg 
+              rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes
+              (List.nth l recno)
            then
             let bo_without_lambdas,_,context =
              eat_lambdas ~subst (tys@context) (recno+1) bo
             in
              (* we assume the formal argument to be safe *)
-             guarded_by_destructors ~subst context (n_plus_len+recno+1)
+             guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context (n_plus_len+recno+1)
               (nn_plus_len+recno+1) kl (x_plus_len+recno+1)
               (1::List.map (fun x -> x+recno+1) safes')
               bo_without_lambdas
            else
-            guarded_by_destructors ~subst (tys@context) n_plus_len nn_plus_len
+            guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst (tys@context) n_plus_len nn_plus_len
              kl x_plus_len safes' bo
          ) (0,true) fl)
    | C.CoFix (_, fl) ->
@@ -993,13 +981,13 @@ and guarded_by_destructors ~subst context n nn kl x safes t =
         List.fold_right
          (fun (_,ty,bo) i ->
            i &&
-            guarded_by_destructors ~subst context n nn kl x_plus_len safes' ty &&
-            guarded_by_destructors ~subst (tys@context) n_plus_len nn_plus_len kl
+            guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x_plus_len safes' ty &&
+            guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst (tys@context) n_plus_len nn_plus_len kl
              x_plus_len safes' bo
          ) fl true
    | C.Appl tl ->
       List.fold_right
-       (fun t i -> i && guarded_by_destructors ~subst context n nn kl x safes t)
+       (fun t i -> i && guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes t)
        tl true
 
 (* the boolean h means already protected *)
@@ -1793,12 +1781,28 @@ end;
 		   let (m, eaten, context') =
 		     eat_lambdas ~subst (types @ context) (x + 1) bo
 		   in
+                   let rec_uri, rec_uri_len = 
+                     match List.hd context' with
+                     | Some (_,Cic.Decl (Cic.MutInd (uri,_,_)))
+                     | Some (_,Cic.Decl (Cic.Appl (Cic.MutInd (uri,_,_)::_))) ->
+                         uri,
+                           (match 
+                            CicEnvironment.get_obj 
+                             CicUniv.oblivion_ugraph uri
+                           with
+                           | Cic.InductiveDefinition (tl,_,_,_), _ ->
+                               List.length tl
+                           | _ -> assert false)
+                     | _ -> assert false
+                   in
 		     (*
 		       let's control the guarded by 
 		       destructors conditions D{f,k,x,M}
 		     *)
-		     if not (guarded_by_destructors ~subst context' eaten 
-			       (len + eaten) kl 1 [] m) then
+		     if not (guarded_by_destructors ~logger ~metasenv ~subst 
+                       rec_uri rec_uri_len context' eaten (len + eaten) kl 
+                       1 [] m) 
+                     then
 		       raise
 			 (TypeCheckerFailure 
 			   (lazy ("Fix: not guarded by destructors:"^CicPp.ppterm t)))
diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.mli b/helm/software/components/cic_proof_checking/cicTypeChecker.mli
index 26dfce388..e1c113ef3 100644
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.mli
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.mli
@@ -34,7 +34,8 @@ exception AssertFailure of string Lazy.t
    output). The callback is used to relocalize the error messages *)
 val debrujin_constructor :
  ?cb:(Cic.term -> Cic.term -> unit) ->
-  UriManager.uri -> int -> Cic.term -> Cic.term
+ ?check_exp_named_subst: bool ->
+  UriManager.uri -> int -> Cic.context -> Cic.term -> Cic.term
 
 val typecheck : UriManager.uri -> Cic.obj * CicUniv.universe_graph
 
diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index dd5191a15..065dbc33d 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -1942,7 +1942,7 @@ let typecheck metasenv uri obj ~localization_tbl =
            (fun (name,ty) (metasenv,ugraph,res) ->
              let ty =
               CicTypeChecker.debrujin_constructor
-               ~cb:(relocalize localization_tbl) uri typesno ty in
+              ~cb:(relocalize localization_tbl) uri typesno [] ty in
              let ty',_,metasenv,ugraph =
               type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
              let ty' = undebrujin uri typesno tys ty' in