From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 8 May 2002 09:15:42 +0000 (+0000)
Subject: Experimental commit: we can now have definitions in contexts. As a
X-Git-Tag: V_0_3_0_debian_8~109
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=756c1e676368d9addc75438bce97a71e34287f18

Experimental commit: we can now have definitions in contexts. As a
consequence the context is now required by CicReduction.whd
---

diff --git a/helm/ocaml/cic_proof_checking/cicReduction.mli b/helm/ocaml/cic_proof_checking/cicReduction.mli
index d61bc7251..c4332a2ed 100644
--- a/helm/ocaml/cic_proof_checking/cicReduction.mli
+++ b/helm/ocaml/cic_proof_checking/cicReduction.mli
@@ -30,5 +30,5 @@ exception ReferenceToVariable
 exception ReferenceToCurrentProof
 exception ReferenceToInductiveDefinition
 val fdebug : int ref
-val whd : Cic.term -> Cic.term
-val are_convertible : Cic.term -> Cic.term -> bool
+val whd : Cic.context -> Cic.term -> Cic.term
+val are_convertible : Cic.context -> Cic.term -> Cic.term -> bool
diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
index b4296f1c1..1ab5e92bc 100644
--- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
@@ -48,12 +48,16 @@ exception ReferenceToCurrentProof;;
 exception ReferenceToInductiveDefinition;;
 
 (* takes a well-typed term *)
-let whd =
+let whd context =
  let rec whdaux l =
   let module C = Cic in
   let module S = CicSubstitution in
    function
-      C.Rel _ as t -> if l = [] then t else C.Appl (t::l)
+      C.Rel n as t ->
+       (match List.nth context (n-1) with
+           C.Decl _ -> if l = [] then t else C.Appl (t::l)
+         | C.Def bo -> whdaux l (S.lift n bo)
+       )
     | C.Var uri as t ->
        (match CicEnvironment.get_cooked_obj uri 0 with
            C.Definition _ -> raise ReferenceToDefinition
@@ -171,102 +175,109 @@ let whd =
           | None -> if l = [] then t else C.Appl (t::l)
          )
     | C.CoFix (i,fl) as t ->
-       (*CSC vecchio codice
-       let (_,_,body) = List.nth fl i in
-        let body' =
-         let counter = ref (List.length fl) in
-          List.fold_right
-           (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
-           fl
-           body
-        in
-         whdaux l body'
-       *)
        if l = [] then t else C.Appl (t::l)
  in
+(*CSC
+function t ->
+prerr_endline ("PRIMA WHD" ^ CicPp.ppterm t) ; flush stderr ;
+List.iter (function (Cic.Decl t) -> prerr_endline ("Context: " ^ CicPp.ppterm t) | (Cic.Def t) -> prerr_endline ("Context:= " ^ CicPp.ppterm t)) context ; flush stderr ; prerr_endline "<PRIMA WHD" ; flush stderr ;
+let res =
+*)
   whdaux []
+(*CSC
+t in prerr_endline "DOPO WHD" ; flush stderr ; res
+*)
 ;;
 
 (* t1, t2 must be well-typed *)
 let are_convertible =
  let module U = UriManager in
- let rec aux t1 t2 =
- let aux2 t1 t2 =
-  (* this trivial euristic cuts down the total time of about five times ;-) *)
-  (* this because most of the time t1 and t2 are "sintactically" the same   *)
-  if t1 = t2 then
-   true
-  else
-   begin
-    let module C = Cic in
-      match (t1,t2) with
-         (C.Rel n1, C.Rel n2) -> n1 = n2
-       | (C.Var uri1, C.Var uri2) -> U.eq uri1 uri2
-       | (C.Meta n1, C.Meta n2) -> n1 = n2
-       | (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *)
-       | (C.Prod (_,s1,t1), C.Prod(_,s2,t2)) ->
-          aux s1 s2 && aux t1 t2
-       | (C.Lambda (_,s1,t1), C.Lambda(_,s2,t2)) ->
-          aux s1 s2 && aux t1 t2
-       | (C.Appl l1, C.Appl l2) ->
-          (try
-            List.fold_right2 (fun  x y b -> aux x y && b) l1 l2 true 
-           with
-            Invalid_argument _ -> false
-          )
-       | (C.Const (uri1,_), C.Const (uri2,_)) ->
-           (*CSC: questo commento e' chiaro o delirante? Io lo sto scrivendo *)
-           (*CSC: mentre sono delirante, quindi ...                          *)
-           (* WARNING: it is really important that the two cookingsno are not *)
-           (* checked for equality. This allows not to cook an object with no *)
-           (* ingredients only to update the cookingsno. E.g: if a term t has *)
-           (* a reference to a term t1 which does not depend on any variable  *)
-           (* and t1 depends on a term t2 (that can't depend on any variable  *)
-           (* because of t1), then t1 cooked at every level could be the same *)
-           (* as t1 cooked at level 0. Doing so, t2 will be extended in t     *)
-           (* with cookingsno 0 and not 2. But this will not cause any trouble*)
-           (* if here we don't check that the two cookingsno are equal.       *)
-           U.eq uri1 uri2
-       | (C.MutInd (uri1,k1,i1), C.MutInd (uri2,k2,i2)) ->
-           (* WARNIG: see the previous warning *)
-           U.eq uri1 uri2 && i1 = i2
-       | (C.MutConstruct (uri1,_,i1,j1), C.MutConstruct (uri2,_,i2,j2)) ->
-           (* WARNIG: see the previous warning *)
-           U.eq uri1 uri2 && i1 = i2 && j1 = j2
-       | (C.MutCase (uri1,_,i1,outtype1,term1,pl1),
-          C.MutCase (uri2,_,i2,outtype2,term2,pl2)) -> 
-           (* WARNIG: see the previous warning *)
-           (* aux outtype1 outtype2 should be true if aux pl1 pl2 *)
-           U.eq uri1 uri2 && i1 = i2 && aux outtype1 outtype2 &&
-            aux term1 term2 &&
-            List.fold_right2 (fun x y b -> b && aux x y) pl1 pl2 true
-       | (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
-          i1 = i2 &&
-           List.fold_right2
-            (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) b ->
-              b && recindex1 = recindex2 && aux ty1 ty2 && aux bo1 bo2)
-            fl1 fl2 true
-       | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
-          i1 = i2 &&
-           List.fold_right2
-            (fun (_,ty1,bo1) (_,ty2,bo2) b ->
-              b && aux ty1 ty2 && aux bo1 bo2)
-            fl1 fl2 true
-       | (C.Abst _, _) | (_, C.Abst _) | (C.Cast _, _) | (_, C.Cast _)
-       | (C.Implicit, _) | (_, C.Implicit) ->
-          raise (Impossible 3) (* we don't trust our whd ;-) *)
-       | (_,_) -> false
-   end
- in
-  if aux2 t1 t2 then true
-  else
-   begin
-    debug t1 [t2] "PREWHD";
-    let t1' = whd t1 
-    and t2' = whd t2 in
-     debug t1' [t2'] "POSTWHD";
-     aux2 t1' t2'
-   end
+ let rec aux context t1 t2 =
+  let aux2 t1 t2 =
+   (* this trivial euristic cuts down the total time of about five times ;-) *)
+   (* this because most of the time t1 and t2 are "sintactically" the same   *)
+   if t1 = t2 then
+    true
+   else
+    begin
+     let module C = Cic in
+       match (t1,t2) with
+          (C.Rel n1, C.Rel n2) -> n1 = n2
+        | (C.Var uri1, C.Var uri2) -> U.eq uri1 uri2
+        | (C.Meta n1, C.Meta n2) -> n1 = n2
+        | (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *)
+        | (C.Prod (_,s1,t1), C.Prod(_,s2,t2)) ->
+           aux context s1 s2 && aux ((C.Decl s1)::context) t1 t2
+        | (C.Lambda (_,s1,t1), C.Lambda(_,s2,t2)) ->
+           aux context s1 s2 && aux ((C.Decl s1)::context) t1 t2
+        | (C.LetIn (_,s1,t1), C.LetIn(_,s2,t2)) ->
+           aux context s1 s2 && aux ((C.Def s1)::context) t1 t2
+        | (C.Appl l1, C.Appl l2) ->
+           (try
+             List.fold_right2 (fun  x y b -> aux context x y && b) l1 l2 true 
+            with
+             Invalid_argument _ -> false
+           )
+        | (C.Const (uri1,_), C.Const (uri2,_)) ->
+            (*CSC: questo commento e' chiaro o delirante? Io lo sto scrivendo *)
+            (*CSC: mentre sono delirante, quindi ...                          *)
+            (* WARNING: it is really important that the two cookingsno are not*)
+            (* checked for equality. This allows not to cook an object with no*)
+            (* ingredients only to update the cookingsno. E.g: if a term t has*)
+            (* a reference to a term t1 which does not depend on any variable *)
+            (* and t1 depends on a term t2 (that can't depend on any variable *)
+            (* because of t1), then t1 cooked at every level could be the same*)
+            (* as t1 cooked at level 0. Doing so, t2 will be extended in t    *)
+            (* with cookingsno 0 and not 2. But this will not cause any       *)
+            (* trouble if here we don't check that the two cookingsno are     *)
+            (* equal.                                                         *)
+            U.eq uri1 uri2
+        | (C.MutInd (uri1,k1,i1), C.MutInd (uri2,k2,i2)) ->
+            (* WARNIG: see the previous warning *)
+            U.eq uri1 uri2 && i1 = i2
+        | (C.MutConstruct (uri1,_,i1,j1), C.MutConstruct (uri2,_,i2,j2)) ->
+            (* WARNIG: see the previous warning *)
+            U.eq uri1 uri2 && i1 = i2 && j1 = j2
+        | (C.MutCase (uri1,_,i1,outtype1,term1,pl1),
+           C.MutCase (uri2,_,i2,outtype2,term2,pl2)) -> 
+            (* WARNIG: see the previous warning *)
+            (* aux context outtype1 outtype2 should be true if *)
+            (* aux context pl1 pl2 *)
+            U.eq uri1 uri2 && i1 = i2 && aux context outtype1 outtype2 &&
+             aux context term1 term2 &&
+             List.fold_right2 (fun x y b -> b && aux context x y) pl1 pl2 true
+        | (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
+(*CSC: C.Decl e' giusto? *)
+           let tys = List.map (function (_,_,ty,_) -> C.Decl ty) fl1 in
+            i1 = i2 &&
+             List.fold_right2
+              (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) b ->
+                b && recindex1 = recindex2 && aux context ty1 ty2 &&
+                 aux (tys@context) bo1 bo2)
+              fl1 fl2 true
+        | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
+(*CSC: C.Decl e' giusto? *)
+           let tys = List.map (function (_,ty,_) -> C.Decl ty) fl1 in
+            i1 = i2 &&
+             List.fold_right2
+              (fun (_,ty1,bo1) (_,ty2,bo2) b ->
+                b && aux context ty1 ty2 && aux (tys@context) bo1 bo2)
+              fl1 fl2 true
+        | (C.Abst _, _) | (_, C.Abst _) | (C.Cast _, _) | (_, C.Cast _)
+        | (C.Implicit, _) | (_, C.Implicit) ->
+           raise (Impossible 3) (* we don't trust our whd ;-) *)
+        | (_,_) -> false
+    end
+  in
+   if aux2 t1 t2 then true
+   else
+    begin
+     debug t1 [t2] "PREWHD";
+     let t1' = whd context t1 
+     and t2' = whd context t2 in
+      debug t1' [t2'] "POSTWHD";
+      aux2 t1' t2'
+    end
  in
   aux
 ;;
diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 884eb1944..34eb7d23f 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -67,14 +67,15 @@ let rec cooked_type_of_constant uri cookingsno =
        (match uobj with
            C.Definition (_,te,ty,_) ->
              let _ = type_of ty in
-              if not (R.are_convertible (type_of te) ty) then
+              if not (R.are_convertible [] (type_of te) ty) then
                raise (NotWellTyped ("Constant " ^ (U.string_of_uri uri)))
          | C.Axiom (_,ty,_) ->
            (* only to check that ty is well-typed *)
            let _ = type_of ty in ()
          | C.CurrentProof (_,conjs,te,ty) ->
              let _ = type_of_aux' conjs [] ty in
-              if not (R.are_convertible (type_of_aux' conjs [] te) ty) then
+              if not (R.are_convertible [] (type_of_aux' conjs [] te) ty)
+              then
                raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))
          | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
        ) ;
@@ -104,7 +105,7 @@ and type_of_variable uri =
        (match bo with
            None -> ()
          | Some bo ->
-            if not (R.are_convertible (type_of bo) ty) then
+            if not (R.are_convertible [] (type_of bo) ty) then
              raise (NotWellTyped ("Variable " ^ (U.string_of_uri uri)))
        ) ;
        CicEnvironment.set_type_checking_info uri ;
@@ -112,51 +113,57 @@ and type_of_variable uri =
        ty
    |  _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
 
-and does_not_occur n nn te =
+and does_not_occur context n nn te =
  let module C = Cic in
    (*CSC: whd sembra essere superflua perche' un caso in cui l'occorrenza *)
    (*CSC: venga mangiata durante la whd sembra presentare problemi di *)
    (*CSC: universi                                                    *)
-   match CicReduction.whd te with
+   match CicReduction.whd context te with
       C.Rel m when m > n && m <= nn -> false
     | C.Rel _
     | C.Var _
     | C.Meta _
     | C.Sort _
     | C.Implicit -> true
-    | C.Cast (te,ty) -> does_not_occur n nn te && does_not_occur n nn ty
+    | C.Cast (te,ty) ->
+       does_not_occur context n nn te && does_not_occur context n nn ty
     | C.Prod (_,so,dest) ->
-       does_not_occur n nn so && does_not_occur (n + 1) (nn + 1) dest
+       does_not_occur context n nn so &&
+        does_not_occur ((C.Decl so)::context) (n + 1) (nn + 1) dest
     | C.Lambda (_,so,dest) ->
-       does_not_occur n nn so && does_not_occur (n + 1) (nn + 1) dest
+       does_not_occur context n nn so &&
+        does_not_occur ((C.Decl so)::context) (n + 1) (nn + 1) dest
     | C.LetIn (_,so,dest) ->
-       does_not_occur n nn so && does_not_occur (n + 1) (nn + 1) dest
+       does_not_occur context n nn so &&
+        does_not_occur ((C.Def so)::context) (n + 1) (nn + 1) dest
     | C.Appl l ->
-       List.fold_right (fun x i -> i && does_not_occur n nn x) l true
+       List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
     | C.Const _
     | C.Abst _
     | C.MutInd _
     | C.MutConstruct _ -> true
     | C.MutCase (_,_,_,out,te,pl) ->
-       does_not_occur n nn out && does_not_occur n nn te &&
-        List.fold_right (fun x i -> i && does_not_occur n nn x) pl true
+       does_not_occur context n nn out && does_not_occur context n nn te &&
+        List.fold_right (fun x i -> i && does_not_occur context n nn x) pl true
     | C.Fix (_,fl) ->
        let len = List.length fl in
         let n_plus_len = n + len in
         let nn_plus_len = nn + len in
+        let tys = List.map (fun (_,_,ty,_) -> Cic.Decl ty) fl in
          List.fold_right
           (fun (_,_,ty,bo) i ->
-            i && does_not_occur n_plus_len nn_plus_len ty &&
-            does_not_occur n_plus_len nn_plus_len bo
+            i && does_not_occur context n nn ty &&
+            does_not_occur (tys @ context) n_plus_len nn_plus_len bo
           ) fl true
     | C.CoFix (_,fl) ->
        let len = List.length fl in
         let n_plus_len = n + len in
         let nn_plus_len = nn + len in
+        let tys = List.map (fun (_,ty,_) -> Cic.Decl ty) fl in
          List.fold_right
           (fun (_,ty,bo) i ->
-            i && does_not_occur n_plus_len nn_plus_len ty &&
-            does_not_occur n_plus_len nn_plus_len bo
+            i && does_not_occur context n nn ty &&
+            does_not_occur (tys @ context) n_plus_len nn_plus_len bo
           ) fl true
 
 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
@@ -164,52 +171,60 @@ and does_not_occur n nn te =
 (*CSC dei controlli leggermente diversi. Viene invocata solamente dalla  *)
 (*CSC strictly_positive                                                  *)
 (*CSC definizione (giusta???) tratta dalla mail di Hugo ;-)              *)
-and weakly_positive n nn uri te =
+and weakly_positive context n nn uri te =
  let module C = Cic in
+(*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*)
+  let dummy_mutind =
+   C.MutInd (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind",0,0)
+  in
   (*CSC mettere in cicSubstitution *)
-  let rec subst_inductive_type_with_dummy_rel =
+  let rec subst_inductive_type_with_dummy_mutind =
    function
       C.MutInd (uri',_,0) when UriManager.eq uri' uri ->
-       C.Rel 0 (* dummy rel *)
+       dummy_mutind
     | C.Appl ((C.MutInd (uri',_,0))::tl) when UriManager.eq uri' uri ->
-       C.Rel 0 (* dummy rel *)
-    | C.Cast (te,ty) -> subst_inductive_type_with_dummy_rel te
+       dummy_mutind
+    | C.Cast (te,ty) -> subst_inductive_type_with_dummy_mutind te
     | C.Prod (name,so,ta) ->
-       C.Prod (name, subst_inductive_type_with_dummy_rel so,
-        subst_inductive_type_with_dummy_rel ta)
+       C.Prod (name, subst_inductive_type_with_dummy_mutind so,
+        subst_inductive_type_with_dummy_mutind ta)
     | C.Lambda (name,so,ta) ->
-       C.Lambda (name, subst_inductive_type_with_dummy_rel so,
-        subst_inductive_type_with_dummy_rel ta)
+       C.Lambda (name, subst_inductive_type_with_dummy_mutind so,
+        subst_inductive_type_with_dummy_mutind ta)
     | C.Appl tl ->
-       C.Appl (List.map subst_inductive_type_with_dummy_rel tl)
+       C.Appl (List.map subst_inductive_type_with_dummy_mutind tl)
     | C.MutCase (uri,cookingsno,i,outtype,term,pl) ->
        C.MutCase (uri,cookingsno,i,
-        subst_inductive_type_with_dummy_rel outtype,
-        subst_inductive_type_with_dummy_rel term,
-        List.map subst_inductive_type_with_dummy_rel pl)
+        subst_inductive_type_with_dummy_mutind outtype,
+        subst_inductive_type_with_dummy_mutind term,
+        List.map subst_inductive_type_with_dummy_mutind pl)
     | C.Fix (i,fl) ->
        C.Fix (i,List.map (fun (name,i,ty,bo) -> (name,i,
-        subst_inductive_type_with_dummy_rel ty,
-        subst_inductive_type_with_dummy_rel bo)) fl)
+        subst_inductive_type_with_dummy_mutind ty,
+        subst_inductive_type_with_dummy_mutind bo)) fl)
     | C.CoFix (i,fl) ->
        C.CoFix (i,List.map (fun (name,ty,bo) -> (name,
-        subst_inductive_type_with_dummy_rel ty,
-        subst_inductive_type_with_dummy_rel bo)) fl)
+        subst_inductive_type_with_dummy_mutind ty,
+        subst_inductive_type_with_dummy_mutind bo)) fl)
     | t -> t
   in
-  match CicReduction.whd te with
+  match CicReduction.whd context te with
      C.Appl ((C.MutInd (uri',_,0))::tl) when UriManager.eq uri' uri -> true
    | C.MutInd (uri',_,0) when UriManager.eq uri' uri -> true
    | C.Prod (C.Anonimous,source,dest) ->
-      strictly_positive n nn (subst_inductive_type_with_dummy_rel source) &&
-       weakly_positive (n + 1) (nn + 1) uri dest
-   | C.Prod (name,source,dest) when does_not_occur 0 n dest ->
-      (* dummy abstraction, so we behave as in the anonimous case *)
-      strictly_positive n nn (subst_inductive_type_with_dummy_rel source) &&
-       weakly_positive (n + 1) (nn + 1) uri dest
+      strictly_positive context n nn
+       (subst_inductive_type_with_dummy_mutind source) &&
+       weakly_positive ((C.Decl source)::context) (n + 1) (nn + 1) uri dest
+   | C.Prod (name,source,dest) when
+      does_not_occur ((C.Decl source)::context) 0 n dest ->
+       (* dummy abstraction, so we behave as in the anonimous case *)
+       strictly_positive context n nn
+        (subst_inductive_type_with_dummy_mutind source) &&
+        weakly_positive ((C.Decl source)::context) (n + 1) (nn + 1) uri dest
    | C.Prod (_,source,dest) ->
-      does_not_occur n nn (subst_inductive_type_with_dummy_rel source) &&
-       weakly_positive (n + 1) (nn + 1) uri dest
+      does_not_occur context n nn
+       (subst_inductive_type_with_dummy_mutind source)&&
+       weakly_positive ((C.Decl source)::context) (n + 1) (nn + 1) uri dest
    | _ -> raise (NotWellFormedTypeOfInductiveConstructor ("Guess where the error is ;-)"))
 
 (* instantiate_parameters ps (x1:T1)...(xn:Tn)C                             *)
@@ -224,25 +239,25 @@ and instantiate_parameters params c =
    | (C.Cast (te,_), _) -> instantiate_parameters params te
    | (t,l) -> raise (Impossible 1)
 
-and strictly_positive n nn te =
+and strictly_positive context n nn te =
  let module C = Cic in
  let module U = UriManager in
-  match CicReduction.whd te with
+  match CicReduction.whd context te with
      C.Rel _ -> true
    | C.Cast (te,ty) ->
       (*CSC: bisogna controllare ty????*)
-      strictly_positive n nn te
+      strictly_positive context n nn te
    | C.Prod (_,so,ta) ->
-      does_not_occur n nn so &&
-       strictly_positive (n+1) (nn+1) ta
+      does_not_occur context n nn so &&
+       strictly_positive ((C.Decl so)::context) (n+1) (nn+1) ta
    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
-      List.fold_right (fun x i -> i && does_not_occur n nn x) tl true
+      List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
    | C.Appl ((C.MutInd (uri,_,i))::tl) -> 
-      let (ok,paramsno,cl) =
+      let (ok,paramsno,ity,cl) =
        match CicEnvironment.get_obj uri with
            C.InductiveDefinition (tl,_,paramsno) ->
-            let (_,_,_,cl) = List.nth tl i in
-             (List.length tl = 1, paramsno, cl)
+            let (_,_,ity,cl) = List.nth tl i in
+             (List.length tl = 1, paramsno, ity, cl)
          | _ -> raise(WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
       in
        let (params,arguments) = split tl paramsno in
@@ -252,20 +267,20 @@ and strictly_positive n nn te =
        in
         ok &&
          List.fold_right
-          (fun x i -> i && does_not_occur n nn x)
+          (fun x i -> i && does_not_occur context n nn x)
           arguments true &&
          (*CSC: MEGAPATCH3 (sara' quella giusta?)*)
          List.fold_right
           (fun x i ->
             i &&
-             weakly_positive (n+1) (nn+1) uri x
+             weakly_positive ((Cic.Decl ity)::context) (n+1) (nn+1) uri x
           ) cl' true
-   | t -> does_not_occur n nn t
+   | t -> does_not_occur context n nn t
 
 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
-and are_all_occurrences_positive uri indparamsno i n nn te =
+and are_all_occurrences_positive context uri indparamsno i n nn te =
  let module C = Cic in
-  match CicReduction.whd te with
+  match CicReduction.whd context te with
      C.Appl ((C.Rel m)::tl) when m = i ->
       (*CSC: riscrivere fermandosi a 0 *)
       (* let's check if the inductive type is applied at least to *)
@@ -275,13 +290,13 @@ and are_all_occurrences_positive uri indparamsno i n nn te =
         (fun k x ->
           if k = 0 then 0
           else
-           match CicReduction.whd x with
+           match CicReduction.whd context x with
               C.Rel m when m = n - (indparamsno - k) -> k - 1
             | _ -> raise (WrongRequiredArgument (UriManager.string_of_uri uri))
         ) indparamsno tl
       in
        if last = 0 then
-        List.fold_right (fun x i -> i && does_not_occur n nn x) tl true
+        List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
        else
         raise (WrongRequiredArgument (UriManager.string_of_uri uri))
    | C.Rel m when m = i ->
@@ -290,15 +305,19 @@ and are_all_occurrences_positive uri indparamsno i n nn te =
       else
        raise (WrongRequiredArgument (UriManager.string_of_uri uri))
    | C.Prod (C.Anonimous,source,dest) ->
-      strictly_positive n nn source &&
-       are_all_occurrences_positive uri indparamsno (i+1) (n + 1) (nn + 1) dest
-   | C.Prod (name,source,dest) when does_not_occur 0 n dest ->
+      strictly_positive context n nn source &&
+       are_all_occurrences_positive ((C.Decl source)::context) uri indparamsno
+        (i+1) (n + 1) (nn + 1) dest
+   | C.Prod (name,source,dest) when
+      does_not_occur ((C.Decl source)::context) 0 n dest ->
       (* dummy abstraction, so we behave as in the anonimous case *)
-      strictly_positive n nn source &&
-       are_all_occurrences_positive uri indparamsno (i+1) (n + 1) (nn + 1) dest
+      strictly_positive context n nn source &&
+       are_all_occurrences_positive ((C.Decl source)::context) uri indparamsno
+        (i+1) (n + 1) (nn + 1) dest
    | C.Prod (_,source,dest) ->
-      does_not_occur n nn source &&
-       are_all_occurrences_positive uri indparamsno (i+1) (n + 1) (nn + 1) dest
+      does_not_occur context n nn source &&
+       are_all_occurrences_positive ((C.Decl source)::context) uri indparamsno
+        (i+1) (n + 1) (nn + 1) dest
    | _ -> raise (NotWellFormedTypeOfInductiveConstructor (UriManager.string_of_uri uri))
 
 (*CSC: cambiare il nome, torna unit! *)
@@ -317,6 +336,10 @@ and cooked_mutual_inductive_defs uri =
       (* constructors using Prods                                *)
       (*CSC: piccola??? inefficienza                             *)
       let len = List.length itl in
+(*CSC: siamo sicuri che non debba fare anche un List.rev? Il bug *)
+(*CSC: si manifesterebbe solamene con tipi veramente mutualmente *)
+(*CSC: induttivi...                                              *)
+       let tys = List.map (fun (_,_,ty,_) -> Cic.Decl ty) itl in
        let _ =
         List.fold_right
          (fun (_,_,_,cl) i ->
@@ -329,13 +352,15 @@ and cooked_mutual_inductive_defs uri =
               in
                let _ = type_of augmented_term in
                 (* let's check also the positivity conditions *)
-                if not (are_all_occurrences_positive uri indparamsno i 0 len te)
+                if
+                 not
+                  (are_all_occurrences_positive tys uri indparamsno i 0 len te)
                 then
                  raise (NotPositiveOccurrences (U.string_of_uri uri))
                 else
                  match !r with
                     Some _ -> raise (Impossible 2)
-                  | None -> r := Some (recursive_args 0 len te)
+                  | None -> r := Some (recursive_args tys 0 len te)
             ) cl ;
            (i + 1)
         ) itl 1
@@ -391,9 +416,9 @@ and cooked_type_of_mutual_inductive_constr uri cookingsno i j =
          ty
     | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
 
-and recursive_args n nn te =
+and recursive_args context n nn te =
  let module C = Cic in
-  match CicReduction.whd te with
+  match CicReduction.whd context te with
      C.Rel _ -> []
    | C.Var _
    | C.Meta _
@@ -401,7 +426,8 @@ and recursive_args n nn te =
    | C.Implicit
    | C.Cast _ (*CSC ??? *) -> raise (Impossible 3) (* due to type-checking *)
    | C.Prod (_,so,de) ->
-      (not (does_not_occur n nn so))::(recursive_args (n+1) (nn + 1) de)
+      (not (does_not_occur context n nn so)) ::
+       (recursive_args ((C.Decl so)::context) (n+1) (nn + 1) de)
    | C.Lambda _
    | C.LetIn _ -> raise (Impossible 4) (* due to type-checking *)
    | C.Appl _ -> []
@@ -413,12 +439,12 @@ and recursive_args n nn te =
    | C.Fix _
    | C.CoFix _ -> raise (Impossible 6) (* due to type-checking *)
 
-and get_new_safes p c rl safes n nn x =
+and get_new_safes context p c rl safes n nn x =
  let module C = Cic in
  let module U = UriManager in
  let module R = CicReduction in
-  match (R.whd c, R.whd p, rl) with
-     (C.Prod (_,_,ta1), C.Lambda (_,_,ta2), b::tl) ->
+  match (R.whd context c, R.whd context p, rl) with
+     (C.Prod (_,so,ta1), C.Lambda (_,_,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' =
@@ -427,11 +453,12 @@ and get_new_safes p c rl safes n nn x =
         let safes'' =
          if b then 1::safes' else safes'
         in
-         get_new_safes ta2 ta1 tl safes'' (n+1) (nn+1) (x+1)
+         get_new_safes ((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)
+   | (C.Appl _, e, []) -> (e,safes,n,nn,x,context)
    | (_,_,_) ->
       (* CSC: If the next exception is raised, it just means that   *)
       (* CSC: the proof-assistant allows to use very strange things *)
@@ -440,33 +467,32 @@ and get_new_safes p c rl safes n nn x =
       (* CSC: must be considered in this match. (e.g. x = MutCase)  *)
       raise (Impossible 7)
 
-and split_prods n te =
+and split_prods context n te =
  let module C = Cic in
  let module R = CicReduction in
-  match (n, R.whd te) with
-     (0, _) -> [],te
+  match (n, R.whd context te) with
+     (0, _) -> context,te
    | (n, C.Prod (_,so,ta)) when n > 0 ->
-      let (l1,l2) = split_prods (n - 1) ta in
-       (so::l1,l2)
+       split_prods ((C.Decl so)::context) (n - 1) ta
    | (_, _) -> raise (Impossible 8)
 
-and eat_lambdas n te =
+and eat_lambdas context n te =
  let module C = Cic in
  let module R = CicReduction in
-  match (n, R.whd te) with
-     (0, _) -> (te, 0)
-   | (n, C.Lambda (_,_,ta)) when n > 0 ->
-      let (te, k) = eat_lambdas (n - 1) ta in
-       (te, k + 1)
+  match (n, R.whd context te) with
+     (0, _) -> (te, 0, context)
+   | (n, C.Lambda (_,so,ta)) when n > 0 ->
+      let (te, k, context') = eat_lambdas ((C.Decl so)::context) (n - 1) ta in
+       (te, k + 1, context')
    | (_, _) -> raise (Impossible 9)
 
 (*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *)
-and check_is_really_smaller_arg n nn kl x safes te =
+and check_is_really_smaller_arg context n nn kl x safes te =
  (*CSC: forse la whd si puo' fare solo quando serve veramente. *)
  (*CSC: cfr guarded_by_destructors                             *)
  let module C = Cic in
  let module U = UriManager in
- match CicReduction.whd te with
+ match CicReduction.whd context te with
      C.Rel m when List.mem m safes -> true
    | C.Rel _ -> false
    | C.Var _
@@ -483,17 +509,17 @@ and check_is_really_smaller_arg n nn kl x safes te =
         (List.map (fun x -> x + 1) safes) ta*)
    | C.Prod _ -> raise (Impossible 10)
    | C.Lambda (_,so,ta) ->
-      check_is_really_smaller_arg n nn kl x safes so &&
-       check_is_really_smaller_arg (n+1) (nn+1) kl (x+1)
+      check_is_really_smaller_arg context n nn kl x safes so &&
+       check_is_really_smaller_arg ((C.Decl so)::context) (n+1) (nn+1) kl (x+1)
         (List.map (fun x -> x + 1) safes) ta
    | C.LetIn (_,so,ta) ->
-      check_is_really_smaller_arg n nn kl x safes so &&
-       check_is_really_smaller_arg (n+1) (nn+1) kl (x+1)
+      check_is_really_smaller_arg context n nn kl x safes so &&
+       check_is_really_smaller_arg ((C.Def so)::context) (n+1) (nn+1) kl (x+1)
         (List.map (fun x -> x + 1) safes) ta
    | C.Appl (he::_) ->
       (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
       (*CSC: solo perche' non abbiamo trovato controesempi            *)
-      check_is_really_smaller_arg n nn kl x safes he
+      check_is_really_smaller_arg context n nn kl x safes he
    | C.Appl [] -> raise (Impossible 11)
    | C.Const _
    | C.Abst _
@@ -505,17 +531,21 @@ and check_is_really_smaller_arg n nn kl x safes te =
            let (isinductive,paramsno,cl) =
             match CicEnvironment.get_obj uri with
                C.InductiveDefinition (tl,_,paramsno) ->
-                let (_,isinductive,_,cl) = List.nth tl i in
-                 let cl' =
-                  List.map (fun (id,ty,r) -> (id, snd (split_prods paramsno ty), r)) cl
-                 in
-                  (isinductive,paramsno,cl')
+                let tys = List.map (fun (_,_,ty,_) -> Cic.Decl ty) tl in
+                 let (_,isinductive,_,cl) = List.nth tl i in
+                  let cl' =
+                   List.map
+                    (fun (id,ty,r) ->
+                      (id, snd (split_prods tys paramsno ty), r)) cl
+                  in
+                   (isinductive,paramsno,cl')
              | _ ->
                raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
            in
             if not isinductive then
               List.fold_right
-               (fun p i -> i && check_is_really_smaller_arg n nn kl x safes p)
+               (fun p i ->
+                 i && check_is_really_smaller_arg context n nn kl x safes p)
                pl true
             else
               List.fold_right
@@ -527,27 +557,31 @@ and check_is_really_smaller_arg n nn kl x safes te =
                        rl''
                    | None -> raise (Impossible 13)
                  in
-                  let (e,safes',n',nn',x') =
-                   get_new_safes p c rl' safes n nn x
+                  let (e,safes',n',nn',x',context') =
+                   get_new_safes context p c rl' safes n nn x
                   in
                    i &&
-                   check_is_really_smaller_arg n' nn' kl x' safes' e
+                   check_is_really_smaller_arg context' n' nn' kl x' safes' e
                ) (List.combine pl cl) true
         | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
            let (isinductive,paramsno,cl) =
             match CicEnvironment.get_obj uri with
                C.InductiveDefinition (tl,_,paramsno) ->
                 let (_,isinductive,_,cl) = List.nth tl i in
-                 let cl' =
-                  List.map (fun (id,ty,r) -> (id, snd (split_prods paramsno ty), r)) cl
-                 in
+                 let tys = List.map (fun (_,_,ty,_) -> Cic.Decl ty) tl in
+                  let cl' =
+                   List.map
+                    (fun (id,ty,r) ->
+                      (id, snd (split_prods tys paramsno ty), r)) cl
+                  in
                   (isinductive,paramsno,cl')
              | _ ->
                raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
            in
             if not isinductive then
               List.fold_right
-               (fun p i -> i && check_is_really_smaller_arg n nn kl x safes p)
+               (fun p i ->
+                 i && check_is_really_smaller_arg context n nn kl x safes p)
                pl true
             else
               (*CSC: supponiamo come prima che nessun controllo sia necessario*)
@@ -561,66 +595,75 @@ and check_is_really_smaller_arg n nn kl x safes te =
                        rl''
                    | None -> raise (Impossible 14)
                  in
-                  let (e, safes',n',nn',x') =
-                   get_new_safes p c rl' safes n nn x
+                  let (e, safes',n',nn',x',context') =
+                   get_new_safes context p c rl' safes n nn x
                   in
                    i &&
-                   check_is_really_smaller_arg n' nn' kl x' safes' e
+                   check_is_really_smaller_arg context' n' nn' kl x' safes' e
                ) (List.combine pl cl) true
         | _ ->
           List.fold_right
-           (fun p i -> i && check_is_really_smaller_arg n nn kl x safes p)
-           pl true
+           (fun p i ->
+             i && check_is_really_smaller_arg context n nn kl x safes p
+           ) pl true
       )
    | C.Fix (_, fl) ->
       let len = List.length fl in
        let n_plus_len = n + len
        and nn_plus_len = nn + len
        and x_plus_len = x + len
+       (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
+       and tys = List.map (fun (_,_,ty,_) -> C.Decl ty) fl
        and safes' = List.map (fun x -> x + len) safes in
         List.fold_right
          (fun (_,_,ty,bo) i ->
            i &&
-            check_is_really_smaller_arg n_plus_len nn_plus_len kl x_plus_len
-             safes' bo
+            check_is_really_smaller_arg (tys@context) n_plus_len nn_plus_len kl
+             x_plus_len safes' bo
          ) fl true
    | C.CoFix (_, fl) ->
       let len = List.length fl in
        let n_plus_len = n + len
        and nn_plus_len = nn + len
        and x_plus_len = x + len
+       (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
+       and tys = List.map (fun (_,ty,_) -> C.Decl ty) fl
        and safes' = List.map (fun x -> x + len) safes in
         List.fold_right
          (fun (_,ty,bo) i ->
            i &&
-            check_is_really_smaller_arg n_plus_len nn_plus_len kl x_plus_len
-             safes' bo
+            check_is_really_smaller_arg (tys@context) n_plus_len nn_plus_len kl
+             x_plus_len safes' bo
          ) fl true
 
-and guarded_by_destructors n nn kl x safes =
+and guarded_by_destructors context n nn kl x safes =
  let module C = Cic in
  let module U = UriManager in
   function
      C.Rel m when m > n && m <= nn -> false
-   | C.Rel _
+   | C.Rel n ->
+      (match List.nth context (n-1) with
+          C.Decl _ -> true
+        | C.Def bo -> guarded_by_destructors context n nn kl x safes bo
+      )
    | C.Var _
    | C.Meta _
    | C.Sort _
    | C.Implicit -> true
    | C.Cast (te,ty) ->
-      guarded_by_destructors n nn kl x safes te &&
-       guarded_by_destructors n nn kl x safes ty
+      guarded_by_destructors context n nn kl x safes te &&
+       guarded_by_destructors context n nn kl x safes ty
    | C.Prod (_,so,ta) ->
-      guarded_by_destructors n nn kl x safes so &&
-       guarded_by_destructors (n+1) (nn+1) kl (x+1)
+      guarded_by_destructors context n nn kl x safes so &&
+       guarded_by_destructors ((C.Decl so)::context) (n+1) (nn+1) kl (x+1)
         (List.map (fun x -> x + 1) safes) ta
    | C.Lambda (_,so,ta) ->
-      guarded_by_destructors n nn kl x safes so &&
-       guarded_by_destructors (n+1) (nn+1) kl (x+1)
+      guarded_by_destructors context n nn kl x safes so &&
+       guarded_by_destructors ((C.Decl so)::context) (n+1) (nn+1) kl (x+1)
         (List.map (fun x -> x + 1) safes) ta
    | C.LetIn (_,so,ta) ->
-      guarded_by_destructors n nn kl x safes so &&
-       guarded_by_destructors (n+1) (nn+1) kl (x+1)
+      guarded_by_destructors context n nn kl x safes so &&
+       guarded_by_destructors ((C.Def so)::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
@@ -628,11 +671,12 @@ and guarded_by_destructors n nn kl x safes =
        else
         List.fold_right
          (fun param i ->
-           i && guarded_by_destructors n nn kl x safes param
+           i && guarded_by_destructors context n nn kl x safes param
          ) tl true &&
-         check_is_really_smaller_arg n nn kl x safes (List.nth tl k)
+         check_is_really_smaller_arg context n nn kl x safes (List.nth tl k)
    | C.Appl tl ->
-      List.fold_right (fun t i -> i && guarded_by_destructors n nn kl x safes t)
+      List.fold_right
+       (fun t i -> i && guarded_by_destructors context n nn kl x safes t)
        tl true
    | C.Const _
    | C.Abst _
@@ -645,22 +689,26 @@ and guarded_by_destructors n nn kl x safes =
             match CicEnvironment.get_obj uri with
                C.InductiveDefinition (tl,_,paramsno) ->
                 let (_,isinductive,_,cl) = List.nth tl i in
-                 let cl' =
-                  List.map (fun (id,ty,r) -> (id, snd (split_prods paramsno ty), r)) cl
-                 in
-                  (isinductive,paramsno,cl')
+                 let tys = List.map (fun (_,_,ty,_) -> Cic.Decl ty) tl in
+                  let cl' =
+                   List.map
+                    (fun (id,ty,r) ->
+                      (id, snd (split_prods tys paramsno ty), r)) cl
+                  in
+                   (isinductive,paramsno,cl')
              | _ ->
                raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
            in
             if not isinductive then
-             guarded_by_destructors n nn kl x safes outtype &&
-              guarded_by_destructors n nn kl x safes term &&
+             guarded_by_destructors context n nn kl x safes outtype &&
+              guarded_by_destructors 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 n nn kl x safes p)
+               (fun p i ->
+                 i && guarded_by_destructors context n nn kl x safes p)
                pl true
             else
-             guarded_by_destructors n nn kl x safes outtype &&
+             guarded_by_destructors context n nn kl x safes outtype &&
               (*CSC: manca ??? il controllo sul tipo di term? *)
               List.fold_right
                (fun (p,(_,c,rl)) i ->
@@ -671,36 +719,41 @@ and guarded_by_destructors n nn kl x safes =
                        rl''
                    | None -> raise (Impossible 15)
                  in
-                  let (e,safes',n',nn',x') =
-                   get_new_safes p c rl' safes n nn x
+                  let (e,safes',n',nn',x',context') =
+                   get_new_safes context p c rl' safes n nn x
                   in
                    i &&
-                   guarded_by_destructors n' nn' kl x' safes' e
+                   guarded_by_destructors context' n' nn' kl x' safes' e
                ) (List.combine pl cl) true
         | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
            let (isinductive,paramsno,cl) =
             match CicEnvironment.get_obj uri with
                C.InductiveDefinition (tl,_,paramsno) ->
                 let (_,isinductive,_,cl) = List.nth tl i in
-                 let cl' =
-                  List.map (fun (id,ty,r) -> (id, snd (split_prods paramsno ty), r)) cl
-                 in
-                  (isinductive,paramsno,cl')
+                 let tys = List.map (fun (_,_,ty,_) -> Cic.Decl ty) tl in
+                  let cl' =
+                   List.map
+                    (fun (id,ty,r) ->
+                      (id, snd (split_prods tys paramsno ty), r)) cl
+                  in
+                   (isinductive,paramsno,cl')
              | _ ->
                raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
            in
             if not isinductive then
-             guarded_by_destructors n nn kl x safes outtype &&
-              guarded_by_destructors n nn kl x safes term &&
+             guarded_by_destructors context n nn kl x safes outtype &&
+              guarded_by_destructors 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 n nn kl x safes p)
+               (fun p i ->
+                 i && guarded_by_destructors context n nn kl x safes p)
                pl true
             else
-             guarded_by_destructors n nn kl x safes outtype &&
+             guarded_by_destructors context n nn kl x safes outtype &&
               (*CSC: manca ??? il controllo sul tipo di term? *)
               List.fold_right
-               (fun t i -> i && guarded_by_destructors n nn kl x safes t)
+               (fun t i ->
+                 i && guarded_by_destructors context n nn kl x safes t)
                tl true &&
               List.fold_right
                (fun (p,(_,c,rl)) i ->
@@ -711,18 +764,18 @@ and guarded_by_destructors n nn kl x safes =
                        rl''
                    | None -> raise (Impossible 16)
                  in
-                  let (e, safes',n',nn',x') =
-                   get_new_safes p c rl' safes n nn x
+                  let (e, safes',n',nn',x',context') =
+                   get_new_safes context p c rl' safes n nn x
                   in
                    i &&
-                   guarded_by_destructors n' nn' kl x' safes' e
+                   guarded_by_destructors context' n' nn' kl x' safes' e
                ) (List.combine pl cl) true
         | _ ->
-          guarded_by_destructors n nn kl x safes outtype &&
-           guarded_by_destructors n nn kl x safes term &&
+          guarded_by_destructors context n nn kl x safes outtype &&
+           guarded_by_destructors 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 n nn kl x safes p)
+            (fun p i -> i && guarded_by_destructors context n nn kl x safes p)
             pl true
       )
    | C.Fix (_, fl) ->
@@ -730,38 +783,41 @@ and guarded_by_destructors n nn kl x safes =
        let n_plus_len = n + len
        and nn_plus_len = nn + len
        and x_plus_len = x + len
+       (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
+       and tys = List.map (fun (_,_,ty,_) -> C.Decl ty) fl
        and safes' = List.map (fun x -> x + len) safes in
         List.fold_right
          (fun (_,_,ty,bo) i ->
-           i && guarded_by_destructors n_plus_len nn_plus_len kl x_plus_len
-            safes' ty &&
-            guarded_by_destructors n_plus_len nn_plus_len kl x_plus_len
-             safes' bo
+           i && guarded_by_destructors context n nn kl x_plus_len safes' ty &&
+            guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
+             x_plus_len safes' bo
          ) fl true
    | C.CoFix (_, fl) ->
       let len = List.length fl in
        let n_plus_len = n + len
        and nn_plus_len = nn + len
        and x_plus_len = x + len
+       (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
+       and tys = List.map (fun (_,ty,_) -> C.Decl ty) fl
        and safes' = List.map (fun x -> x + len) safes in
         List.fold_right
          (fun (_,ty,bo) i ->
-           i && guarded_by_destructors n_plus_len nn_plus_len kl x_plus_len
-            safes' ty &&
-            guarded_by_destructors n_plus_len nn_plus_len kl x_plus_len safes'
-             bo
+           i &&
+            guarded_by_destructors context n nn kl x_plus_len safes' ty &&
+            guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
+             x_plus_len safes' bo
          ) fl true
 
 (* the boolean h means already protected *)
 (* args is the list of arguments the type of the constructor that may be *)
 (* found in head position must be applied to.                            *)
 (*CSC: coInductiveTypeURI non cambia mai di ricorsione in ricorsione *)
-and guarded_by_constructors n nn h te args coInductiveTypeURI =
+and guarded_by_constructors context n nn h te args coInductiveTypeURI =
  let module C = Cic in
   (*CSC: There is a lot of code replication between the cases X and    *)
   (*CSC: (C.Appl X tl). Maybe it will be better to define a function   *)
   (*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *)
-  match CicReduction.whd te with
+  match CicReduction.whd context te with
      C.Rel m when m > n && m <= nn -> h
    | C.Rel _
    | C.Var _  -> true
@@ -773,11 +829,12 @@ and guarded_by_constructors n nn h te args coInductiveTypeURI =
    | C.LetIn _ ->
       raise (Impossible 17) (* the term has just been type-checked *)
    | C.Lambda (_,so,de) ->
-      does_not_occur n nn so &&
-       guarded_by_constructors (n + 1) (nn + 1) h de args coInductiveTypeURI
+      does_not_occur context n nn so &&
+       guarded_by_constructors ((C.Decl so)::context) (n + 1) (nn + 1) h de args
+        coInductiveTypeURI
    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
       h &&
-       List.fold_right (fun x i -> i && does_not_occur n nn x) tl true
+       List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
    | C.Appl ((C.MutConstruct (uri,cookingsno,i,j))::tl) ->
       let consty =
        match CicEnvironment.get_cooked_obj uri cookingsno with
@@ -788,32 +845,32 @@ and guarded_by_constructors n nn h te args coInductiveTypeURI =
          raise (WrongUriToMutualInductiveDefinitions
           (UriManager.string_of_uri uri))
       in
-       let rec analyse_branch ty te =
-        match CicReduction.whd ty with
+       let rec analyse_branch context ty te =
+        match CicReduction.whd context ty with
            C.Meta _ -> raise (Impossible 34)
          | C.Rel _
          | C.Var _
          | C.Sort _ ->
-            does_not_occur n nn te
+            does_not_occur context n nn te
          | C.Implicit
          | C.Cast _ -> raise (Impossible 24) (* due to type-checking *)
-         | C.Prod (_,_,de) ->
-            analyse_branch de te
+         | C.Prod (_,so,de) ->
+            analyse_branch ((C.Decl so)::context) de te
          | C.Lambda _
          | C.LetIn _ -> raise (Impossible 25) (* due to type-checking *)
          | C.Appl ((C.MutInd (uri,_,_))::tl) as ty
             when uri == coInductiveTypeURI -> 
-             guarded_by_constructors n nn true te [] coInductiveTypeURI
+             guarded_by_constructors context n nn true te [] coInductiveTypeURI
          | C.Appl ((C.MutInd (uri,_,_))::tl) as ty -> 
-            guarded_by_constructors n nn true te tl coInductiveTypeURI
+            guarded_by_constructors context n nn true te tl coInductiveTypeURI
          | C.Appl _ ->
-            does_not_occur n nn te
+            does_not_occur context n nn te
          | C.Const _
          | C.Abst _ -> raise (Impossible 26)
          | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
-            guarded_by_constructors n nn true te [] coInductiveTypeURI
+            guarded_by_constructors context n nn true te [] coInductiveTypeURI
          | C.MutInd _ ->
-            does_not_occur n nn te
+            does_not_occur context n nn te
          | C.MutConstruct _ -> raise (Impossible 27)
          (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
          (*CSC: in head position.                                       *)
@@ -821,8 +878,8 @@ and guarded_by_constructors n nn h te args coInductiveTypeURI =
          | C.Fix _
          | C.CoFix _ -> raise (Impossible 28) (* due to type-checking *)
        in
-       let rec analyse_instantiated_type ty l =
-        match CicReduction.whd ty with
+       let rec analyse_instantiated_type context ty l =
+        match CicReduction.whd context ty with
            C.Rel _
          | C.Var _
          | C.Meta _
@@ -834,17 +891,19 @@ and guarded_by_constructors n nn h te args coInductiveTypeURI =
              match l with
                 [] -> true
               | he::tl ->
-                 analyse_branch so he &&
-                  analyse_instantiated_type de tl
+                 analyse_branch context so he &&
+                  analyse_instantiated_type ((C.Decl so)::context) de tl
             end
          | C.Lambda _
          | C.LetIn _ -> raise (Impossible 30) (* due to type-checking *)
          | C.Appl _ -> 
-            List.fold_left (fun i x -> i && does_not_occur n nn x) true l
+            List.fold_left
+             (fun i x -> i && does_not_occur context n nn x) true l
          | C.Const _
          | C.Abst _ -> raise (Impossible 31)
          | C.MutInd _ ->
-            List.fold_left (fun i x -> i && does_not_occur n nn x) true l
+            List.fold_left
+             (fun i x -> i && does_not_occur context n nn x) true l
          | C.MutConstruct _ -> raise (Impossible 32)
          (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
          (*CSC: in head position.                                       *)
@@ -856,7 +915,7 @@ and guarded_by_constructors n nn h te args coInductiveTypeURI =
          function
             [] -> true
           | tlhe::tltl as l ->
-             let consty' = CicReduction.whd consty in
+             let consty' = CicReduction.whd context consty in
               match args with 
                  he::tl ->
                   begin
@@ -864,78 +923,84 @@ and guarded_by_constructors n nn h te args coInductiveTypeURI =
                       C.Prod (_,_,de) ->
                        let instantiated_de = CicSubstitution.subst he de in
                         (*CSC: siamo sicuri che non sia troppo forte? *)
-                        does_not_occur n nn tlhe &
+                        does_not_occur context n nn tlhe &
                          instantiate_type tl instantiated_de tltl
                     | _ ->
                       (*CSC:We do not consider backbones with a MutCase, a    *)
                       (*CSC:FixPoint, a CoFixPoint and so on in head position.*)
                       raise (Impossible 23)
                   end
-               | [] -> analyse_instantiated_type consty' l
+               | [] -> analyse_instantiated_type context consty' l
                   (* These are all the other cases *)
        in
         instantiate_type args consty tl
    | C.Appl ((C.CoFix (_,fl))::tl) ->
-      List.fold_left (fun i x -> i && does_not_occur n nn x) true tl &&
+      List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
        let len = List.length fl in
         let n_plus_len = n + len
-        and nn_plus_len = nn + len in
+        and nn_plus_len = nn + len
+        (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
+        and tys = List.map (fun (_,ty,_) -> C.Decl ty) fl in
          List.fold_right
           (fun (_,ty,bo) i ->
-            i && does_not_occur n_plus_len nn_plus_len ty &&
-             guarded_by_constructors n_plus_len nn_plus_len h bo args
-              coInductiveTypeURI
+            i && does_not_occur context n nn ty &&
+             guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
+              args coInductiveTypeURI
           ) fl true
    | C.Appl ((C.MutCase (_,_,_,out,te,pl))::tl) ->
-       List.fold_left (fun i x -> i && does_not_occur n nn x) true tl &&
-        does_not_occur n nn out &&
-         does_not_occur n nn te &&
+       List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
+        does_not_occur context n nn out &&
+         does_not_occur context n nn te &&
           List.fold_right
            (fun x i ->
              i &&
-             guarded_by_constructors n nn h x args coInductiveTypeURI
+             guarded_by_constructors context n nn h x args coInductiveTypeURI
            ) pl true
    | C.Appl l ->
-      List.fold_right (fun x i -> i && does_not_occur n nn x) l true
+      List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
    | C.Const _ -> true
    | C.Abst _
    | C.MutInd _ -> assert false
    | C.MutConstruct _ -> true
    | C.MutCase (_,_,_,out,te,pl) ->
-       does_not_occur n nn out &&
-        does_not_occur n nn te &&
+       does_not_occur context n nn out &&
+        does_not_occur context n nn te &&
          List.fold_right
           (fun x i ->
             i &&
-             guarded_by_constructors n nn h x args coInductiveTypeURI
+             guarded_by_constructors context n nn h x args coInductiveTypeURI
           ) pl true
    | C.Fix (_,fl) ->
       let len = List.length fl in
        let n_plus_len = n + len
-       and nn_plus_len = nn + len in
+       and nn_plus_len = nn + len
+       (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
+       and tys = List.map (fun (_,_,ty,_) -> C.Decl ty) fl in
         List.fold_right
          (fun (_,_,ty,bo) i ->
-           i && does_not_occur n_plus_len nn_plus_len ty &&
-            does_not_occur n_plus_len nn_plus_len bo
+           i && does_not_occur context n nn ty &&
+            does_not_occur (tys@context) n_plus_len nn_plus_len bo
          ) fl true
    | C.CoFix (_,fl) ->
       let len = List.length fl in
        let n_plus_len = n + len
-       and nn_plus_len = nn + len in
+       and nn_plus_len = nn + len
+       (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
+       and tys = List.map (fun (_,ty,_) -> C.Decl ty) fl in
         List.fold_right
          (fun (_,ty,bo) i ->
-           i && does_not_occur n_plus_len nn_plus_len ty &&
-            guarded_by_constructors n_plus_len nn_plus_len h bo args
-             coInductiveTypeURI
+           i && does_not_occur context n nn ty &&
+            guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
+             args coInductiveTypeURI
          ) fl true
 
-and check_allowed_sort_elimination uri i need_dummy ind arity1 arity2 =
+and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 =
  let module C = Cic in
  let module U = UriManager in
-  match (CicReduction.whd arity1, CicReduction.whd arity2) with
+  match (CicReduction.whd context arity1, CicReduction.whd context arity2) with
      (C.Prod (_,so1,de1), C.Prod (_,so2,de2))
-      when CicReduction.are_convertible so1 so2 ->
-       check_allowed_sort_elimination uri i need_dummy
+      when CicReduction.are_convertible context so1 so2 ->
+       check_allowed_sort_elimination context uri i need_dummy
         (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2
    | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true
    | (C.Sort C.Prop, C.Sort C.Set) when need_dummy ->
@@ -952,17 +1017,19 @@ and check_allowed_sort_elimination uri i need_dummy ind arity1 arity2 =
    | (C.Sort C.Set, C.Sort C.Type) when need_dummy ->
        (match CicEnvironment.get_obj uri with
            C.InductiveDefinition (itl,_,paramsno) ->
-            let (_,_,_,cl) = List.nth itl i in
-             List.fold_right (fun (_,x,_) i -> i && is_small paramsno x) cl true
+            let tys = List.map (fun (_,_,ty,_) -> Cic.Decl ty) itl in
+             let (_,_,_,cl) = List.nth itl i in
+              List.fold_right
+               (fun (_,x,_) i -> i && is_small tys paramsno x) cl true
          | _ ->
            raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
        )
    | (C.Sort C.Type, C.Sort _) when need_dummy -> true
    | (C.Sort C.Prop, C.Prod (_,so,ta)) when not need_dummy ->
-       let res = CicReduction.are_convertible so ind
+       let res = CicReduction.are_convertible context so ind
        in
         res &&
-        (match CicReduction.whd ta with
+        (match CicReduction.whd ((C.Decl so)::context) ta with
             C.Sort C.Prop -> true
           | C.Sort C.Set ->
              (match CicEnvironment.get_obj uri with
@@ -977,18 +1044,19 @@ and check_allowed_sort_elimination uri i need_dummy ind arity1 arity2 =
           | _ -> false
         )
    | (C.Sort C.Set, C.Prod (_,so,ta)) when not need_dummy ->
-       let res = CicReduction.are_convertible so ind
+       let res = CicReduction.are_convertible context so ind
        in
         res &&
-        (match CicReduction.whd ta with
+        (match CicReduction.whd ((C.Decl so)::context) ta with
             C.Sort C.Prop
           | C.Sort C.Set  -> true
           | C.Sort C.Type ->
              (match CicEnvironment.get_obj uri with
                  C.InductiveDefinition (itl,_,paramsno) ->
                   let (_,_,_,cl) = List.nth itl i in
-                   List.fold_right
-                    (fun (_,x,_) i -> i && is_small paramsno x) cl true
+                   let tys = List.map (fun (_,_,ty,_) -> Cic.Decl ty) itl in
+                    List.fold_right
+                     (fun (_,x,_) i -> i && is_small tys paramsno x) cl true
                | _ ->
                  raise (WrongUriToMutualInductiveDefinitions
                   (U.string_of_uri uri))
@@ -996,13 +1064,13 @@ and check_allowed_sort_elimination uri i need_dummy ind arity1 arity2 =
           | _ -> raise (Impossible 19)
         )
    | (C.Sort C.Type, C.Prod (_,so,_)) when not need_dummy ->
-       CicReduction.are_convertible so ind
+       CicReduction.are_convertible context so ind
    | (_,_) -> false
   
-and type_of_branch argsno need_dummy outtype term constype =
+and type_of_branch context argsno need_dummy outtype term constype =
  let module C = Cic in
  let module R = CicReduction in
-  match R.whd constype with
+  match R.whd context constype with
      C.MutInd (_,_,_) ->
       if need_dummy then
        outtype
@@ -1016,8 +1084,8 @@ and type_of_branch argsno need_dummy outtype term constype =
        else
         C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
    | C.Prod (name,so,de) ->
-      C.Prod (C.Name "pippo",so,type_of_branch argsno need_dummy 
-       (CicSubstitution.lift 1 outtype)
+      C.Prod (C.Anonimous,so,type_of_branch ((C.Decl so)::context) argsno
+       need_dummy (CicSubstitution.lift 1 outtype)
        (C.Appl [CicSubstitution.lift 1 term ; C.Rel 1]) de)
   | _ -> raise (Impossible 20)
        
@@ -1031,13 +1099,13 @@ and type_of_aux' metasenv context t =
   let module U = UriManager in
    function
       C.Rel n ->
-       let t =
-        try
-         List.nth context (n - 1)
+       (try
+         match List.nth context (n - 1) with
+            C.Decl t -> S.lift n t
+          | C.Def bo -> type_of_aux context (S.lift n bo)
         with
          _ -> raise (NotWellTyped "Not a close term")
-       in
-        S.lift n t
+       )
     | C.Var uri ->
       incr fdebug ;
       let ty = type_of_variable uri in
@@ -1048,16 +1116,16 @@ and type_of_aux' metasenv context t =
     | C.Implicit -> raise (Impossible 21)
     | C.Cast (te,ty) ->
        let _ = type_of_aux context ty in
-        if R.are_convertible (type_of_aux context te) ty then ty
+        if R.are_convertible context (type_of_aux context te) ty then ty
         else raise (NotWellTyped "Cast")
     | C.Prod (_,s,t) ->
        let sort1 = type_of_aux context s
-       and sort2 = type_of_aux (s::context) t in
+       and sort2 = type_of_aux ((C.Decl s)::context) t in
         sort_of_prod (sort1,sort2)
    | C.Lambda (n,s,t) ->
        let sort1 = type_of_aux context s
-       and type2 = type_of_aux (s::context) t in
-        let sort2 = type_of_aux (s::context) type2 in
+       and type2 = type_of_aux ((C.Decl s)::context) t in
+        let sort2 = type_of_aux ((C.Decl s)::context) type2 in
          (* only to check if the product is well-typed *)
          let _ = sort_of_prod (sort1,sort2) in
           C.Prod (n,s,type2)
@@ -1067,7 +1135,7 @@ and type_of_aux' metasenv context t =
    | C.Appl (he::tl) when List.length tl > 0 ->
       let hetype = type_of_aux context he
       and tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in
-       eat_prods hetype tlbody_and_type
+       eat_prods context hetype tlbody_and_type
    | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
    | C.Const (uri,cookingsno) ->
       incr fdebug ;
@@ -1087,14 +1155,14 @@ and type_of_aux' metasenv context t =
    | C.MutCase (uri,cookingsno,i,outtype,term,pl) ->
       let outsort = type_of_aux context outtype in
       let (need_dummy, k) =
-       let rec guess_args t =
-        match CicReduction.whd t with
+       let rec guess_args context t =
+        match CicReduction.whd context t with
            C.Sort _ -> (true, 0)
          | C.Prod (_, s, t) ->
-            let (b, n) = guess_args t in
+            let (b, n) = guess_args ((C.Decl s)::context) t in
              if n = 0 then
               (* last prod before sort *)
-              match CicReduction.whd s with
+              match CicReduction.whd context s with
                  (*CSC vedi nota delirante su cookingsno in cicReduction.ml *)
                  C.MutInd (uri',_,i') when U.eq uri' uri && i' = i -> (false, 1)
                | C.Appl ((C.MutInd (uri',_,i')) :: _)
@@ -1105,11 +1173,11 @@ and type_of_aux' metasenv context t =
          | _ -> raise (NotWellTyped "MutCase: outtype ill-formed")
        in
         (*CSC whd non serve dopo type_of_aux ? *)
-        let (b, k) = guess_args outsort in
+        let (b, k) = guess_args context outsort in
          if not b then (b, k - 1) else (b, k)
       in
       let (parameters, arguments) =
-        match R.whd (type_of_aux context term) with
+        match R.whd context (type_of_aux context term) with
            (*CSC manca il caso dei CAST *)
            C.MutInd (uri',_,i') ->
             (*CSC vedi nota delirante sui cookingsno in cicReduction.ml*)
@@ -1133,7 +1201,7 @@ and type_of_aux' metasenv context t =
         else
          C.Appl ((C.MutInd (uri,cookingsno,i))::parameters)
        in
-        if not (check_allowed_sort_elimination uri i need_dummy
+        if not (check_allowed_sort_elimination context uri i need_dummy
          sort_of_ind_type (type_of_aux context sort_of_ind_type) outsort)
         then
          raise (NotWellTyped "MutCase: not allowed sort elimination") ;
@@ -1156,8 +1224,8 @@ and type_of_aux' metasenv context t =
                (C.Appl (C.MutConstruct (uri,cookingsno,i,j)::parameters))
              in
               (j + 1, b &&
-               R.are_convertible (type_of_aux context p)
-                (type_of_branch parsno need_dummy outtype cons
+               R.are_convertible context (type_of_aux context p)
+                (type_of_branch context parsno need_dummy outtype cons
                   (type_of_aux context cons))
               )
            ) (1,true) (List.combine pl cl)
@@ -1175,19 +1243,26 @@ and type_of_aux' metasenv context t =
       let types_times_kl =
        List.rev
         (List.map
-          (fun (_,k,ty,_) -> let _ = type_of_aux context ty in (ty,k)) fl)
+          (fun (_,k,ty,_) ->
+            let _ = type_of_aux context ty in (C.Decl ty,k)) fl)
       in
       let (types,kl) = List.split types_times_kl in
        let len = List.length types in
         List.iter
          (fun (name,x,ty,bo) ->
-           if (R.are_convertible (type_of_aux (types @ context) bo)
-            (CicSubstitution.lift len ty))
+           if
+            (R.are_convertible (types@context) (type_of_aux (types@context) bo)
+             (CicSubstitution.lift len ty))
            then
             begin
-             let (m, eaten) = eat_lambdas (x + 1) bo in
+             let (m, eaten, context') =
+              eat_lambdas (types @ context) (x + 1) bo
+             in
               (*let's control the guarded by destructors conditions D{f,k,x,M}*)
-              if not (guarded_by_destructors eaten (len + eaten) kl 1 [] m) then
+              if
+               not
+                (guarded_by_destructors context' eaten (len + eaten) kl 1 [] m)
+              then
                raise (NotWellTyped "Fix: not guarded by destructors")
             end
            else
@@ -1200,13 +1275,15 @@ and type_of_aux' metasenv context t =
    | C.CoFix (i,fl) ->
       let types =
        List.rev
-        (List.map (fun (_,ty,_) -> let _ = type_of_aux context ty in ty) fl)
+        (List.map
+          (fun (_,ty,_) -> let _ = type_of_aux context ty in C.Decl ty) fl)
       in
        let len = List.length types in
         List.iter
          (fun (_,ty,bo) ->
-           if (R.are_convertible (type_of_aux (types @ context) bo)
-            (CicSubstitution.lift len ty))
+           if
+            (R.are_convertible (types @ context)
+             (type_of_aux (types @ context) bo) (CicSubstitution.lift len ty))
            then
             begin
              (* let's control that the returned type is coinductive *)
@@ -1215,7 +1292,11 @@ and type_of_aux' metasenv context t =
                  raise(NotWellTyped "CoFix: does not return a coinductive type")
               | Some uri ->
                  (*let's control the guarded by constructors conditions C{f,M}*)
-                 if not (guarded_by_constructors 0 len false bo [] uri) then
+                 if
+                  not
+                   (guarded_by_constructors (types @ context) 0 len false bo
+                     [] uri)
+                 then
                   raise (NotWellTyped "CoFix: not guarded by constructors")
             end
            else
@@ -1227,8 +1308,8 @@ and type_of_aux' metasenv context t =
 
  and sort_of_prod (t1, t2) =
   let module C = Cic in
-   let t1' = CicReduction.whd t1 in
-   let t2' = CicReduction.whd t2 in
+   let t1' = CicReduction.whd context t1 in
+   let t2' = CicReduction.whd context t2 in
    match (t1', t2') with
       (C.Sort s1, C.Sort s2)
         when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *)
@@ -1239,22 +1320,22 @@ and type_of_aux' metasenv context t =
        (NotWellTyped
         ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= " ^ CicPp.ppterm t2'))
 
- and eat_prods hetype =
+ and eat_prods context hetype =
   (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
   (*CSC: cucinati                                                         *)
   function
      [] -> hetype
    | (hete, hety)::tl ->
-    (match (CicReduction.whd hetype) with
+    (match (CicReduction.whd context hetype) with
         Cic.Prod (n,s,t) ->
-         if CicReduction.are_convertible s hety then
+         if CicReduction.are_convertible context s hety then
           (CicReduction.fdebug := -1 ;
-           eat_prods (CicSubstitution.subst hete t) tl
+           eat_prods context (CicSubstitution.subst hete t) tl
           )
          else
           begin
            CicReduction.fdebug := 0 ;
-           ignore (CicReduction.are_convertible s hety) ;
+           ignore (CicReduction.are_convertible context s hety) ;
            fdebug := 0 ;
            debug s [hety] ;
            raise (NotWellTyped "Appl: wrong parameter-type")
@@ -1264,7 +1345,7 @@ and type_of_aux' metasenv context t =
 
  and returns_a_coinductive ty =
   let module C = Cic in
-   match CicReduction.whd ty with
+   match CicReduction.whd context ty with
       C.MutInd (uri,cookingsno,i) ->
        (*CSC: definire una funzioncina per questo codice sempre replicato *)
        (match CicEnvironment.get_cooked_obj uri cookingsno with
@@ -1288,26 +1369,40 @@ and type_of_aux' metasenv context t =
     | _ -> None
 
  in
+(*CSC
+prerr_endline ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t) ; flush stderr ;
+let res =
+*)
   type_of_aux context t
+(*
+in prerr_endline "FINE TYPE_OF_AUX" ; flush stderr ; res
+*)
 
 (* is a small constructor? *)
 (*CSC: ottimizzare calcolando staticamente *)
-and is_small paramsno c =
+and is_small context paramsno c =
  let rec is_small_aux context c =
   let module C = Cic in
-   match CicReduction.whd c with
+   match CicReduction.whd context c with
       C.Prod (_,so,de) ->
        (*CSC: [] is an empty metasenv. Is it correct? *)
        let s = type_of_aux' [] context so in
         (s = C.Sort C.Prop || s = C.Sort C.Set) &&
-        is_small_aux (so::context) de
+        is_small_aux ((C.Decl so)::context) de
     | _ -> true (*CSC: we trust the type-checker *)
  in
-  let (sx,dx) = split_prods paramsno c in
-   is_small_aux (List.rev sx) dx
+  let (context',dx) = split_prods context paramsno c in
+   is_small_aux context' dx
 
 and type_of t =
+(*CSC
+prerr_endline ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t) ; flush stderr ;
+let res =
+*)
  type_of_aux' [] [] t
+(*CSC
+in prerr_endline "FINE TYPE_OF_AUX'" ; flush stderr ; res
+*)
 ;;
 
 let typecheck uri =
@@ -1322,7 +1417,7 @@ let typecheck uri =
       (match uobj with
           C.Definition (_,te,ty,_) ->
            let _ = type_of ty in
-            if not (R.are_convertible (type_of te ) ty) then
+            if not (R.are_convertible [] (type_of te ) ty) then
              raise (NotWellTyped ("Constant " ^ (U.string_of_uri uri)))
         | C.Axiom (_,ty,_) ->
           (* only to check that ty is well-typed *)
@@ -1331,7 +1426,7 @@ let typecheck uri =
 	    (*CSC [] wrong *)
             let _ = type_of_aux' conjs [] ty in
              debug (type_of_aux' conjs [] te) [] ;
-             if not (R.are_convertible (type_of_aux' conjs [] te) ty) then
+             if not (R.are_convertible [] (type_of_aux' conjs [] te) ty) then
               raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))
         | C.Variable (_,bo,ty) ->
            (* only to check that ty is well-typed *)
@@ -1339,7 +1434,7 @@ let typecheck uri =
             (match bo with
                 None -> ()
               | Some bo ->
-                 if not (R.are_convertible (type_of bo) ty) then
+                 if not (R.are_convertible [] (type_of bo) ty) then
                   raise (NotWellTyped ("Variable" ^ (U.string_of_uri uri)))
             )
         | C.InductiveDefinition _ ->
@@ -1348,20 +1443,3 @@ let typecheck uri =
       CicEnvironment.set_type_checking_info uri ;
       Logger.log (`Type_checking_completed uri)
 ;;
-
-(*******************************************************)
-(*CSC: Da qua in avanti deve sparire tutto *)
-exception NotImplemented
-let wrong_context_of_context context =
- let module C = Cic in
-  List.map
-   (function
-       C.Decl bt -> bt
-     | C.Def bt -> raise NotImplemented
-   ) context
-;;
-
-let type_of_aux' metasenv context t =
- let context' = wrong_context_of_context context in
-  type_of_aux' metasenv context' t
-;;
diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index ce7aa5280..4126d0446 100644
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -130,7 +130,7 @@ let fo_unif_new metasenv context t1 t2 =
        | (C.Sort _ ,_)
        | (_, C.Sort _)
        | (C.Implicit, _)
-       | (_, C.Implicit) -> if R.are_convertible t1 t2 then subst
+       | (_, C.Implicit) -> if R.are_convertible context t1 t2 then subst
                             else raise UnificationFailed
        | (C.Cast (te,ty), t2) -> fo_unif_aux subst k te t2
        | (t1, C.Cast (te,ty)) -> fo_unif_aux subst k t1 te
@@ -163,7 +163,7 @@ let fo_unif_new metasenv context t1 t2 =
        | (C.MutInd  _, _) 
        | (_, C.MutInd _)
        | (C.MutConstruct _, _)
-       | (_, C.MutConstruct _) -> if R.are_convertible t1 t2 then subst
+       | (_, C.MutConstruct _) -> if R.are_convertible context t1 t2 then subst
                                    else raise UnificationFailed
        | (C.MutCase (_,_,_,outt1,t1,pl1), C.MutCase (_,_,_,outt2,t2,pl2))->
                       let subst' = fo_unif_aux subst k outt1 outt2 in
@@ -172,7 +172,7 @@ let fo_unif_new metasenv context t1 t2 =
        | (C.Fix _, _)
        | (_, C.Fix _) 
        | (C.CoFix _, _)
-       | (_, C.CoFix _) -> if R.are_convertible t1 t2 then subst
+       | (_, C.CoFix _) -> if R.are_convertible context t1 t2 then subst
                            else raise UnificationFailed
        | (_,_) -> raise UnificationFailed
    in fo_unif_aux [] 0 t1 t2;;