]> matita.cs.unibo.it Git - helm.git/commitdiff
~subst fixed everywhere in the type-checker:
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 25 Oct 2005 11:11:40 +0000 (11:11 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 25 Oct 2005 11:11:40 +0000 (11:11 +0000)
 1. sometimes it was not passed to functions
 2. sometimes it was passed but it was not used/useful/correct
 3. sometimes it was not passed recursively

helm/ocaml/cic_proof_checking/cicTypeChecker.ml

index b24c5fc8e7b2b4e3cd50074a2bb1560220445c72..007962097e03b95c2f8318937e8f93f30f61e4b9 100644 (file)
@@ -232,42 +232,47 @@ and type_of_variable ~logger uri ugraph =
    |  _ ->
        raise (TypeCheckerFailure ("Unknown variable:" ^ U.string_of_uri uri))
 
-and does_not_occur context n nn te =
+and does_not_occur ?(subst=[]) 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 context te with
+   match CicReduction.whd ~subst context te with
       C.Rel m when m > n && m <= nn -> false
     | C.Rel _
-    | C.Meta _  (* CSC: Are we sure? No recursion?*)
     | C.Sort _
     | C.Implicit _ -> true
+    | C.Meta (_,l) ->
+       List.fold_right
+        (fun x i ->
+          match x with
+             None -> i
+           | Some x -> i && does_not_occur ~subst context n nn x) l true
     | C.Cast (te,ty) ->
-       does_not_occur context n nn te && does_not_occur context n nn ty
+       does_not_occur ~subst context n nn te && does_not_occur ~subst context n nn ty
     | C.Prod (name,so,dest) ->
-       does_not_occur context n nn so &&
-        does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
-         dest
+       does_not_occur ~subst context n nn so &&
+        does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n + 1)
+         (nn + 1) dest
     | C.Lambda (name,so,dest) ->
-       does_not_occur context n nn so &&
-        does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
+       does_not_occur ~subst context n nn so &&
+        does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
          dest
     | C.LetIn (name,so,dest) ->
-       does_not_occur context n nn so &&
-        does_not_occur ((Some (name,(C.Def (so,None))))::context)
+       does_not_occur ~subst context n nn so &&
+        does_not_occur ~subst ((Some (name,(C.Def (so,None))))::context)
          (n + 1) (nn + 1) dest
     | C.Appl l ->
-       List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
+       List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) l true
     | C.Var (_,exp_named_subst)
     | C.Const (_,exp_named_subst)
     | C.MutInd (_,_,exp_named_subst)
     | C.MutConstruct (_,_,_,exp_named_subst) ->
-       List.fold_right (fun (_,x) i -> i && does_not_occur context n nn x)
+       List.fold_right (fun (_,x) i -> i && does_not_occur ~subst context n nn x)
         exp_named_subst true
     | C.MutCase (_,_,out,te,pl) ->
-       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
+       does_not_occur ~subst context n nn out && does_not_occur ~subst context n nn te &&
+        List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) pl true
     | C.Fix (_,fl) ->
        let len = List.length fl in
         let n_plus_len = n + len in
@@ -277,8 +282,8 @@ and does_not_occur context n nn te =
         in
          List.fold_right
           (fun (_,_,ty,bo) i ->
-            i && does_not_occur context n nn ty &&
-            does_not_occur (tys @ context) n_plus_len nn_plus_len bo
+            i && does_not_occur ~subst context n nn ty &&
+            does_not_occur ~subst (tys @ context) n_plus_len nn_plus_len bo
           ) fl true
     | C.CoFix (_,fl) ->
        let len = List.length fl in
@@ -289,8 +294,8 @@ and does_not_occur context n nn te =
         in
          List.fold_right
           (fun (_,ty,bo) i ->
-            i && does_not_occur context n nn ty &&
-            does_not_occur (tys @ context) n_plus_len nn_plus_len bo
+            i && does_not_occur ~subst context n nn ty &&
+            does_not_occur ~subst (tys @ context) n_plus_len nn_plus_len bo
           ) fl true
 
 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
@@ -304,7 +309,7 @@ and weakly_positive context n nn uri te =
   let dummy_mutind =
    C.MutInd (HelmLibraryObjects.Datatypes.nat_URI,0,[])
   in
-  (*CSC mettere in cicSubstitution *)
+  (*CSC: mettere in cicSubstitution *)
   let rec subst_inductive_type_with_dummy_mutind =
    function
       C.MutInd (uri',0,_) when UriManager.eq uri' uri ->
@@ -438,7 +443,7 @@ and strictly_positive context n nn te =
           ) cl' true
    | t -> does_not_occur context n nn t
 
-(*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
+(* the inductive type indexes are s.t. n < x <= nn *)
 and are_all_occurrences_positive context uri indparamsno i n nn te =
  let module C = Cic in
   match CicReduction.whd context te with
@@ -647,7 +652,7 @@ and recursive_args context n nn te =
    | C.Fix _
    | C.CoFix _ -> raise (AssertFailure "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 c rl safes n nn x =
  let module C = Cic in
  let module U = UriManager in
  let module R = CicReduction in
@@ -678,16 +683,16 @@ and get_new_safes ?(subst = []) context p c rl safes n nn x =
          (Printf.sprintf "Get New Safes: c=%s ; p=%s"
            (CicPp.ppterm c) (CicPp.ppterm p)))
 
-and split_prods ?(subst = []) context n te =
+and split_prods ~subst context n te =
  let module C = Cic in
  let module R = CicReduction in
-  match (n, R.whd context te) with
+  match (n, R.whd ~subst context te) with
      (0, _) -> context,te
    | (n, C.Prod (name,so,ta)) when n > 0 ->
        split_prods ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta
    | (_, _) -> raise (AssertFailure "8")
 
-and eat_lambdas ?(subst = []) context n te =
+and eat_lambdas ~subst context n te =
  let module C = Cic in
  let module R = CicReduction in
   match (n, R.whd ~subst context te) with
@@ -701,12 +706,12 @@ and eat_lambdas ?(subst = []) context n te =
        raise (AssertFailure (sprintf "9 (%d, %s)" n (CicPp.ppterm te)))
 
 (*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *) 
-and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te =
+and check_is_really_smaller_arg ~subst 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 context te with
+ match CicReduction.whd ~subst context te with
      C.Rel m when List.mem m safes -> true
    | C.Rel _ -> false
    | C.Var _
@@ -829,7 +834,7 @@ and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te =
                    recursive_args tys 0 len debrujinedte
                  in
                   let (e, safes',n',nn',x',context') =
-                   get_new_safes context p c rl' safes n nn x
+                   get_new_safes ~subst context p c rl' safes n nn x
                   in
                    i &&
                    check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
@@ -867,7 +872,7 @@ and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te =
              x_plus_len safes' bo
          ) fl true
 
-and guarded_by_destructors ?(subst = []) context n nn kl x safes =
+and guarded_by_destructors ~subst context n nn kl x safes =
  let module C = Cic in
  let module U = UriManager in
   function
@@ -876,7 +881,7 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes =
       (match List.nth context (n-1) with
           Some (_,C.Decl _) -> true
         | Some (_,C.Def (bo,_)) ->
-           guarded_by_destructors context m nn kl x safes
+           guarded_by_destructors ~subst context m nn kl x safes
             (CicSubstitution.lift m bo)
         | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
       )
@@ -884,19 +889,19 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes =
    | C.Sort _
    | C.Implicit _ -> true
    | C.Cast (te,ty) ->
-      guarded_by_destructors context n nn kl x safes te &&
-       guarded_by_destructors context n nn kl x safes ty
+      guarded_by_destructors ~subst context n nn kl x safes te &&
+       guarded_by_destructors ~subst context n nn kl x safes ty
    | C.Prod (name,so,ta) ->
-      guarded_by_destructors context n nn kl x safes so &&
-       guarded_by_destructors ((Some (name,(C.Decl so)))::context)
+      guarded_by_destructors ~subst context n nn kl x safes so &&
+       guarded_by_destructors ~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 context n nn kl x safes so &&
-       guarded_by_destructors ((Some (name,(C.Decl so)))::context)
+      guarded_by_destructors ~subst context n nn kl x safes so &&
+       guarded_by_destructors ~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,ta) ->
-      guarded_by_destructors context n nn kl x safes so &&
-       guarded_by_destructors ((Some (name,(C.Def (so,None))))::context)
+      guarded_by_destructors ~subst context n nn kl x safes so &&
+       guarded_by_destructors ~subst ((Some (name,(C.Def (so,None))))::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
@@ -904,22 +909,22 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes =
        else
         List.fold_right
          (fun param i ->
-           i && guarded_by_destructors context n nn kl x safes param
+           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)
    | C.Appl tl ->
       List.fold_right
-       (fun t i -> i && guarded_by_destructors context n nn kl x safes t)
+       (fun t i -> i && guarded_by_destructors ~subst context n nn kl x safes t)
        tl true
    | C.Var (_,exp_named_subst)
    | C.Const (_,exp_named_subst)
    | C.MutInd (_,_,exp_named_subst)
    | C.MutConstruct (_,_,_,exp_named_subst) ->
       List.fold_right
-       (fun (_,t) i -> i && guarded_by_destructors context n nn kl x safes t)
+       (fun (_,t) i -> i && guarded_by_destructors ~subst context n nn kl x safes t)
        exp_named_subst true
    | C.MutCase (uri,i,outtype,term,pl) ->
-      (match CicReduction.whd context term with
+      (match CicReduction.whd ~subst context term with
           C.Rel m when List.mem m safes || m = x ->
            let (tys,len,isinductive,paramsno,cl) =
            let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
@@ -946,12 +951,12 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes =
                   UriManager.string_of_uri uri))
            in
             if not isinductive then
-             guarded_by_destructors context n nn kl x safes outtype &&
-              guarded_by_destructors context n nn kl x safes term &&
+             guarded_by_destructors ~subst context n nn kl x safes outtype &&
+              guarded_by_destructors ~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 context n nn kl x safes p)
+                 i && guarded_by_destructors ~subst context n nn kl x safes p)
                pl true
             else
              let pl_and_cl =
@@ -961,16 +966,16 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes =
                Invalid_argument _ ->
                 raise (TypeCheckerFailure "not enough patterns")
              in
-             guarded_by_destructors context n nn kl x safes outtype &&
+             guarded_by_destructors ~subst context n nn kl x safes outtype &&
               (*CSC: manca ??? il controllo sul tipo di term? *)
               List.fold_right
                (fun (p,(_,c,brujinedc)) i ->
                  let rl' = recursive_args tys 0 len brujinedc in
                   let (e,safes',n',nn',x',context') =
-                   get_new_safes context p c rl' safes n nn x
+                   get_new_safes ~subst context p c rl' safes n nn x
                   in
                    i &&
-                   guarded_by_destructors context' n' nn' kl x' safes' e
+                   guarded_by_destructors ~subst context' n' nn' kl x' safes' e
                ) pl_and_cl true
         | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
            let (tys,len,isinductive,paramsno,cl) =
@@ -994,12 +999,12 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes =
                   UriManager.string_of_uri uri))
            in
             if not isinductive then
-             guarded_by_destructors context n nn kl x safes outtype &&
-              guarded_by_destructors context n nn kl x safes term &&
+             guarded_by_destructors ~subst context n nn kl x safes outtype &&
+              guarded_by_destructors ~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 context n nn kl x safes p)
+                 i && guarded_by_destructors ~subst context n nn kl x safes p)
                pl true
             else
              let pl_and_cl =
@@ -1009,11 +1014,11 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes =
                Invalid_argument _ ->
                 raise (TypeCheckerFailure "not enough patterns")
              in
-             guarded_by_destructors context n nn kl x safes outtype &&
+             guarded_by_destructors ~subst 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 context n nn kl x safes t)
+                 i && guarded_by_destructors ~subst context n nn kl x safes t)
                tl true &&
               List.fold_right
                (fun (p,(_,c)) i ->
@@ -1022,17 +1027,17 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes =
                    recursive_args tys 0 len debrujinedte
                  in
                   let (e, safes',n',nn',x',context') =
-                   get_new_safes context p c rl' safes n nn x
+                   get_new_safes ~subst context p c rl' safes n nn x
                   in
                    i &&
-                   guarded_by_destructors context' n' nn' kl x' safes' e
+                   guarded_by_destructors ~subst context' n' nn' kl x' safes' e
                ) pl_and_cl true
         | _ ->
-          guarded_by_destructors context n nn kl x safes outtype &&
-           guarded_by_destructors context n nn kl x safes term &&
+          guarded_by_destructors ~subst context n nn kl x safes outtype &&
+           guarded_by_destructors ~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 context n nn kl x safes p)
+            (fun p i -> i && guarded_by_destructors ~subst context n nn kl x safes p)
             pl true
       )
    | C.Fix (_, fl) ->
@@ -1044,8 +1049,8 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes =
        and safes' = List.map (fun x -> x + len) safes in
         List.fold_right
          (fun (_,_,ty,bo) i ->
-           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
+           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
              x_plus_len safes' bo
          ) fl true
    | C.CoFix (_, fl) ->
@@ -1058,21 +1063,20 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes =
         List.fold_right
          (fun (_,ty,bo) i ->
            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
+            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
              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 context n nn h te args coInductiveTypeURI =
+and guarded_by_constructors ~subst 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 context te with
+  match CicReduction.whd ~subst context te with
      C.Rel m when m > n && m <= nn -> h
    | C.Rel _ -> true
    | C.Meta _
@@ -1084,12 +1088,12 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI =
       (* the term has just been type-checked *)
       raise (AssertFailure "17")
    | C.Lambda (name,so,de) ->
-      does_not_occur context n nn so &&
-       guarded_by_constructors ((Some (name,(C.Decl so)))::context)
+      does_not_occur ~subst context n nn so &&
+       guarded_by_constructors ~subst ((Some (name,(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 context n nn x) tl true
+       List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) tl true
    | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) ->
       let consty =
        let obj,_ = 
@@ -1107,12 +1111,12 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI =
               UriManager.string_of_uri uri))
       in
        let rec analyse_branch context ty te =
-        match CicReduction.whd context ty with
+        match CicReduction.whd ~subst context ty with
            C.Meta _ -> raise (AssertFailure "34")
          | C.Rel _
          | C.Var _
          | C.Sort _ ->
-            does_not_occur context n nn te
+            does_not_occur ~subst context n nn te
          | C.Implicit _
          | C.Cast _ ->
             raise (AssertFailure "24")(* due to type-checking *)
@@ -1123,16 +1127,19 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI =
             raise (AssertFailure "25")(* due to type-checking *)
          | C.Appl ((C.MutInd (uri,_,_))::_) as ty
             when uri == coInductiveTypeURI -> 
-             guarded_by_constructors context n nn true te [] coInductiveTypeURI
+             guarded_by_constructors ~subst context n nn true te []
+              coInductiveTypeURI
          | C.Appl ((C.MutInd (uri,_,_))::_) as ty -> 
-            guarded_by_constructors context n nn true te tl coInductiveTypeURI
+            guarded_by_constructors ~subst context n nn true te tl
+             coInductiveTypeURI
          | C.Appl _ ->
-            does_not_occur context n nn te
+            does_not_occur ~subst context n nn te
          | C.Const _ -> raise (AssertFailure "26")
          | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
-            guarded_by_constructors context n nn true te [] coInductiveTypeURI
+            guarded_by_constructors ~subst context n nn true te []
+             coInductiveTypeURI
          | C.MutInd _ ->
-            does_not_occur context n nn te
+            does_not_occur ~subst context n nn te
          | C.MutConstruct _ -> raise (AssertFailure "27")
          (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
          (*CSC: in head position.                                       *)
@@ -1142,7 +1149,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI =
             raise (AssertFailure "28")(* due to type-checking *)
        in
        let rec analyse_instantiated_type context ty l =
-        match CicReduction.whd context ty with
+        match CicReduction.whd ~subst context ty with
            C.Rel _
          | C.Var _
          | C.Meta _
@@ -1163,11 +1170,11 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI =
             raise (AssertFailure "30")(* due to type-checking *)
          | C.Appl _ -> 
             List.fold_left
-             (fun i x -> i && does_not_occur context n nn x) true l
+             (fun i x -> i && does_not_occur ~subst context n nn x) true l
          | C.Const _ -> raise (AssertFailure "31")
          | C.MutInd _ ->
             List.fold_left
-             (fun i x -> i && does_not_occur context n nn x) true l
+             (fun i x -> i && does_not_occur ~subst context n nn x) true l
          | C.MutConstruct _ -> raise (AssertFailure "32")
          (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
          (*CSC: in head position.                                       *)
@@ -1180,7 +1187,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI =
          function
             [] -> true
           | tlhe::tltl as l ->
-             let consty' = CicReduction.whd context consty in
+             let consty' = CicReduction.whd ~subst context consty in
               match args with 
                  he::tl ->
                   begin
@@ -1188,7 +1195,7 @@ and guarded_by_constructors context 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 context n nn tlhe &
+                        does_not_occur ~subst context n nn tlhe &
                          instantiate_type tl instantiated_de tltl
                     | _ ->
                       (*CSC:We do not consider backbones with a MutCase, a    *)
@@ -1200,7 +1207,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI =
        in
         instantiate_type args consty tl
    | C.Appl ((C.CoFix (_,fl))::tl) ->
-      List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
+      List.fold_left (fun i x -> i && does_not_occur ~subst context n nn x) true tl &&
        let len = List.length fl in
         let n_plus_len = n + len
         and nn_plus_len = nn + len
@@ -1208,36 +1215,38 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI =
         and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
          List.fold_right
           (fun (_,ty,bo) i ->
-            i && does_not_occur context n nn ty &&
-             guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
-              args coInductiveTypeURI
+            i && does_not_occur ~subst context n nn ty &&
+             guarded_by_constructors ~subst (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 context n nn x) true tl &&
-        does_not_occur context n nn out &&
-         does_not_occur context n nn te &&
+       List.fold_left (fun i x -> i && does_not_occur ~subst context n nn x) true tl &&
+        does_not_occur ~subst context n nn out &&
+         does_not_occur ~subst context n nn te &&
           List.fold_right
            (fun x i ->
              i &&
-             guarded_by_constructors context n nn h x args coInductiveTypeURI
+             guarded_by_constructors ~subst context n nn h x args
+              coInductiveTypeURI
            ) pl true
    | C.Appl l ->
-      List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
+      List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) l true
    | C.Var (_,exp_named_subst)
    | C.Const (_,exp_named_subst) ->
       List.fold_right
-       (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
+       (fun (_,x) i -> i && does_not_occur ~subst context n nn x) exp_named_subst true
    | C.MutInd _ -> assert false
    | C.MutConstruct (_,_,_,exp_named_subst) ->
       List.fold_right
-       (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
+       (fun (_,x) i -> i && does_not_occur ~subst context n nn x) exp_named_subst true
    | C.MutCase (_,_,out,te,pl) ->
-       does_not_occur context n nn out &&
-        does_not_occur context n nn te &&
+       does_not_occur ~subst context n nn out &&
+        does_not_occur ~subst context n nn te &&
          List.fold_right
           (fun x i ->
             i &&
-             guarded_by_constructors context n nn h x args coInductiveTypeURI
+             guarded_by_constructors ~subst context n nn h x args
+              coInductiveTypeURI
           ) pl true
    | C.Fix (_,fl) ->
       let len = List.length fl in
@@ -1247,8 +1256,8 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI =
        and tys = List.map (fun (n,_,ty,_)-> Some (C.Name n,(C.Decl ty))) fl in
         List.fold_right
          (fun (_,_,ty,bo) i ->
-           i && does_not_occur context n nn ty &&
-            does_not_occur (tys@context) n_plus_len nn_plus_len bo
+           i && does_not_occur ~subst context n nn ty &&
+            does_not_occur ~subst (tys@context) n_plus_len nn_plus_len bo
          ) fl true
    | C.CoFix (_,fl) ->
       let len = List.length fl in
@@ -1258,8 +1267,9 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI =
        and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
         List.fold_right
          (fun (_,ty,bo) i ->
-           i && does_not_occur context n nn ty &&
-            guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
+           i && does_not_occur ~subst context n nn ty &&
+            guarded_by_constructors ~subst (tys@context) n_plus_len nn_plus_len
+             h bo
              args coInductiveTypeURI
          ) fl true
 
@@ -1384,10 +1394,10 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
        CicReduction.are_convertible ~subst ~metasenv context so ind ugraph
    | (_,_) -> false,ugraph
         
-and type_of_branch context argsno need_dummy outtype term constype =
+and type_of_branch ~subst context argsno need_dummy outtype term constype =
  let module C = Cic in
  let module R = CicReduction in
-  match R.whd context constype with
+  match R.whd ~subst context constype with
      C.MutInd (_,_,_) ->
       if need_dummy then
        outtype
@@ -1406,7 +1416,7 @@ and type_of_branch context argsno need_dummy outtype term constype =
           C.Appl l -> C.Appl (l@[C.Rel 1])
         | t -> C.Appl [t ; C.Rel 1]
       in
-       C.Prod (C.Anonymous,so,type_of_branch
+       C.Prod (C.Anonymous,so,type_of_branch ~subst
         ((Some (name,(C.Decl so)))::context) argsno need_dummy
         (CicSubstitution.lift 1 outtype) term' de)
   | _ -> raise (AssertFailure "20")
@@ -1416,7 +1426,7 @@ metavariable is consitent - up to relocation via the relocation list l -
 with the actual context *)
 
 
-and check_metasenv_consistency ~logger ?(subst=[]) metasenv context 
+and check_metasenv_consistency ~logger ~subst metasenv context 
   canonical_context l ugraph 
 =
   let module C = Cic in
@@ -1573,7 +1583,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
        (* The type of the LetIn is reduced. Much faster than the previous
           solution. Moreover the inferred type is probably very different
           from the expected one.
-       (CicReduction.whd context
+       (CicReduction.whd ~subst context
         (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)))
        *)
        (* One-step LetIn reduction. Even faster than the previous solution.
@@ -1665,7 +1675,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
 (*
       let (parameters, arguments, exp_named_subst),ugraph2 =
        let ty,ugraph2 = type_of_aux context term ugraph1 in
-          match R.whd context ty with
+          match R.whd ~subst context ty with
            (*CSC manca il caso dei CAST *)
 (*CSC: ma servono i parametri (uri,i)? Se si', perche' non serve anche il *)
 (*CSC: parametro exp_named_subst? Se no, perche' non li togliamo?         *)
@@ -1780,7 +1790,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
              let ty_cons,ugraph3 = type_of_aux ~logger context cons ugraph1 in
              (* 2 is skipped *)
              let ty_branch = 
-               type_of_branch context parsno need_dummy outtype cons 
+               type_of_branch ~subst context parsno need_dummy outtype cons 
                  ty_cons in
              let b1,ugraph4 =
                R.are_convertible 
@@ -1835,7 +1845,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
                       let's control the guarded by 
                       destructors conditions D{f,k,x,M}
                     *)
-                    if not (guarded_by_destructors context' eaten 
+                    if not (guarded_by_destructors ~subst context' eaten 
                               (len + eaten) kl 1 [] m) then
                       raise
                         (TypeCheckerFailure 
@@ -1872,7 +1882,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
                if b then
                  begin
                    (* let's control that the returned type is coinductive *)
-                   match returns_a_coinductive context ty with
+                   match returns_a_coinductive ~subst context ty with
                        None ->
                          raise
                          (TypeCheckerFailure
@@ -1882,8 +1892,8 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
                            let's control the guarded by constructors 
                            conditions C{f,M}
                          *)
-                         if not (guarded_by_constructors (types @ context) 
-                                   0 len false bo [] uri) then
+                         if not (guarded_by_constructors ~subst
+                              (types @ context) 0 len false bo [] uri) then
                            raise
                              (TypeCheckerFailure 
                                 ("CoFix: not guarded by constructors"))
@@ -1898,7 +1908,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
        let (_,ty,_) = List.nth fl i in
         ty,ugraph2
 
- and check_exp_named_subst ~logger ?(subst = []) context ugraph =
+ and check_exp_named_subst ~logger ~subst context ugraph =
    let rec check_exp_named_subst_aux ~logger esubsts l ugraph =
      match l with
         [] -> ugraph
@@ -1926,7 +1936,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
    in
      check_exp_named_subst_aux ~logger [] ugraph 
        
- and sort_of_prod ?(subst = []) context (name,s) (t1, t2) ugraph =
+ and sort_of_prod ~subst context (name,s) (t1, t2) ugraph =
   let module C = Cic in
    let t1' = CicReduction.whd ~subst context t1 in
    let t2' = CicReduction.whd ~subst ((Some (name,C.Decl s))::context) t2 in
@@ -1952,7 +1962,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
         "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1')
           (CicPp.ppterm t2')))
 
- and eat_prods ?(subst = []) context hetype l ugraph =
+ and eat_prods ~subst context hetype l ugraph =
    (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
    (*CSC: cucinati                                                         *)
    match l with
@@ -1989,9 +1999,9 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
                         "Appl: this is not a function, it cannot be applied")
         )
 
- and returns_a_coinductive context ty =
+ and returns_a_coinductive ~subst context ty =
   let module C = Cic in
-   match CicReduction.whd context ty with
+   match CicReduction.whd ~subst context ty with
       C.MutInd (uri,i,_) ->
        (*CSC: definire una funzioncina per questo codice sempre replicato *)
         let obj,_ =
@@ -2020,7 +2030,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
               UriManager.string_of_uri uri))
         )
     | C.Prod (n,so,de) ->
-       returns_a_coinductive ((Some (n,C.Decl so))::context) de
+       returns_a_coinductive ~subst ((Some (n,C.Decl so))::context) de
     | _ -> None
 
  in
@@ -2040,7 +2050,6 @@ and is_small ~logger context paramsno c ugraph =
   let module C = Cic in
    match CicReduction.whd context c with
       C.Prod (n,so,de) ->
-       (*CSC: [] is an empty metasenv. Is it correct? *)
        let s,ugraph1 = type_of_aux' ~logger [] context so ugraph in
        let b = (s = C.Sort C.Prop || s = C.Sort C.Set || s = C.Sort C.CProp) in
        if b then
@@ -2049,7 +2058,7 @@ and is_small ~logger context paramsno c ugraph =
                 false,ugraph1
     | _ -> true,ugraph (*CSC: we trust the type-checker *)
  in
-  let (context',dx) = split_prods context paramsno c in
+  let (context',dx) = split_prods ~subst:[] context paramsno c in
    is_small_aux ~logger context' dx ugraph
 
 and type_of ~logger t ugraph =