]> matita.cs.unibo.it Git - helm.git/commitdiff
moved the expansion of implicits inside the refiner in a lazy way
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 25 Oct 2005 15:49:18 +0000 (15:49 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 25 Oct 2005 15:49:18 +0000 (15:49 +0000)
helm/ocaml/cic_disambiguation/disambiguate.ml
helm/ocaml/cic_proof_checking/cicReduction.ml
helm/ocaml/cic_proof_checking/cicTypeChecker.ml
helm/ocaml/cic_unification/cicMkImplicit.ml
helm/ocaml/cic_unification/cicMkImplicit.mli
helm/ocaml/cic_unification/cicRefine.ml

index 7e0996f4f59ef693050b9aef47d03b941c56934a..f203e6d790edc4b2cc6e413afa8e1c40c6935964 100644 (file)
@@ -62,8 +62,6 @@ type 'a test_result =
 let refine_term metasenv context uri term ugraph =
 (*   if benchmark then incr actual_refinements; *)
   assert (uri=None);
-  let metasenv, term = 
-    CicMkImplicit.expand_implicits metasenv [] context term in
     debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term)));
     try
       let term', _, metasenv',ugraph1 = 
@@ -80,7 +78,6 @@ let refine_term metasenv context uri term ugraph =
 
 let refine_obj metasenv context uri obj ugraph =
  assert (context = []);
- let metasenv, obj = CicMkImplicit.expand_implicits_in_obj metasenv [] obj in
    debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj))) ;
    try
      let obj', metasenv,ugraph = CicRefine.typecheck metasenv uri obj in
index 0229f23386bf39d0d0ed3a5cee7b8f1919c05760..39133ac92a4beb9ce9a5bbd87c4ca2f27387fc79 100644 (file)
@@ -1006,8 +1006,7 @@ let are_convertible whd ?(subst=[]) ?(metasenv=[])  =
             else
               false,ugraph
         | (C.Cast _, _) | (_, C.Cast _)
-        | (C.Implicit _, _) | (_, C.Implicit _) ->
-            assert false
+        | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
         | (_,_) -> false,ugraph
     end
   in
index 605b9676e2d5befe11e590de052ed9651d4dac9f..2f7075dacf34fca1004e1a1aeb7d7bcf50c1d851 100644 (file)
@@ -460,7 +460,8 @@ and are_all_occurrences_positive context uri indparamsno i n nn te =
               C.Rel m when m = n - (indparamsno - k) -> k - 1
             | _ ->
               raise (TypeCheckerFailure
-                (lazy ("Non-positive occurence in mutual inductive definition(s) " ^
+               (lazy 
+               ("Non-positive occurence in mutual inductive definition(s) [1]" ^
                 UriManager.string_of_uri uri)))
         ) indparamsno tl
       in
@@ -468,14 +469,14 @@ and are_all_occurrences_positive context uri indparamsno i n nn te =
         List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
        else
         raise (TypeCheckerFailure
-          (lazy ("Non-positive occurence in mutual inductive definition(s) " ^
+         (lazy ("Non-positive occurence in mutual inductive definition(s) [2]"^
           UriManager.string_of_uri uri)))
    | C.Rel m when m = i ->
       if indparamsno = 0 then
        true
       else
         raise (TypeCheckerFailure
-          (lazy ("Non-positive occurence in mutual inductive definition(s) " ^
+         (lazy ("Non-positive occurence in mutual inductive definition(s) [3]"^
           UriManager.string_of_uri uri)))
    | C.Prod (C.Anonymous,source,dest) ->
       strictly_positive context n nn source &&
index a2d0a73d54bbf09ecf10da7b08a2512f9c42dbbf..bc60a188d201ce11c13f6957d0e4c9ab882f9481 100644 (file)
@@ -118,196 +118,3 @@ let fresh_subst metasenv subst context uris =
           (uri,Cic.Meta(newmeta+2,irl))::l in
     aux newmeta uris
 
-let expand_implicits metasenv subst context term =
-  let rec aux metasenv context = function
-    | (Cic.Rel _) as t -> metasenv, t
-    | (Cic.Sort _) as t -> metasenv, t
-    | Cic.Const (uri, subst) ->
-        let metasenv', subst' = do_subst metasenv context subst in
-        metasenv', Cic.Const (uri, subst')
-    | Cic.Var (uri, subst) ->
-        let metasenv', subst' = do_subst metasenv context subst in
-        metasenv', Cic.Var (uri, subst')
-    | Cic.MutInd (uri, i, subst) ->
-        let metasenv', subst' = do_subst metasenv context subst in
-        metasenv', Cic.MutInd (uri, i, subst')
-    | Cic.MutConstruct (uri, i, j, subst) ->
-        let metasenv', subst' = do_subst metasenv context subst in
-        metasenv', Cic.MutConstruct (uri, i, j, subst')
-    | Cic.Meta (n,l) -> 
-        let metasenv', l' = do_local_context metasenv context l in
-        metasenv', Cic.Meta (n, l')
-    | Cic.Implicit (Some `Type) ->
-        let (metasenv', idx) = mk_implicit_type metasenv subst context in
-        let irl = identity_relocation_list_for_metavariable context in
-        metasenv', Cic.Meta (idx, irl)
-    | Cic.Implicit (Some `Closed) ->
-        let (metasenv', idx) = mk_implicit metasenv subst [] in
-        metasenv', Cic.Meta (idx, [])
-    | Cic.Implicit None ->
-        let (metasenv', idx) = mk_implicit metasenv subst context in
-        let irl = identity_relocation_list_for_metavariable context in
-        metasenv', Cic.Meta (idx, irl)
-    | Cic.Implicit _ -> assert false
-    | Cic.Cast (te, ty) ->
-        let metasenv', ty' = aux metasenv context ty in
-        let metasenv'', te' = aux metasenv' context te in
-        metasenv'', Cic.Cast (te', ty')
-    | Cic.Prod (name, s, t) ->
-        let metasenv', s' = aux metasenv context s in
-        let metasenv'', t' =
-          aux metasenv' (Some (name, Cic.Decl s') :: context) t
-        in
-        metasenv'', Cic.Prod (name, s', t')
-    | Cic.Lambda (name, s, t) ->
-        let metasenv', s' = aux metasenv context s in
-        let metasenv'', t' =
-          aux metasenv' (Some (name, Cic.Decl s') :: context) t
-        in
-        metasenv'', Cic.Lambda (name, s', t')
-    | Cic.LetIn (name, s, t) ->
-        let metasenv', s' = aux metasenv context s in
-        let metasenv'', t' =
-          aux metasenv' (Some (name, Cic.Def (s', None)) :: context) t
-        in
-        metasenv'', Cic.LetIn (name, s', t')
-    | Cic.Appl l when List.length l > 1 ->
-        let metasenv', l' =
-          List.fold_right
-            (fun term (metasenv, terms) ->
-              let new_metasenv, term = aux metasenv context term in
-              new_metasenv, term :: terms)
-            l (metasenv, [])
-        in
-        metasenv', Cic.Appl l'
-    | Cic.Appl _ -> assert false
-    | Cic.MutCase (uri, i, outtype, term, patterns) ->
-        let metasenv', l' =
-          List.fold_right
-            (fun term (metasenv, terms) ->
-              let new_metasenv, term = aux metasenv context term in
-              new_metasenv, term :: terms)
-            (outtype :: term :: patterns) (metasenv, [])
-        in
-        let outtype', term', patterns' =
-          match l' with
-          | outtype' :: term' :: patterns' -> outtype', term', patterns'
-          | _ -> assert false
-        in
-        metasenv', Cic.MutCase (uri, i, outtype', term', patterns')
-    | Cic.Fix (i, funs) ->
-        let metasenv', types =
-          List.fold_right
-            (fun (name, _, typ, _) (metasenv, types) ->
-              let new_metasenv, new_type = aux metasenv context typ in
-              (new_metasenv, (name, new_type) :: types))
-            funs (metasenv, [])
-        in
-        let context' =
-          (List.rev_map
-            (fun (name, t) -> Some (Cic.Name name, Cic.Decl t))
-            types)
-          @ context
-        in
-        let metasenv'', bodies =
-          List.fold_right
-            (fun (_, _, _, body) (metasenv, bodies) ->
-              let new_metasenv, new_body = aux metasenv context' body in
-              (new_metasenv, new_body :: bodies))
-            funs (metasenv', [])
-        in
-        let rec combine = function
-          | ((name, index, _, _) :: funs_tl),
-            ((_, typ) :: typ_tl),
-            (body :: body_tl) ->
-              (name, index, typ, body) :: combine (funs_tl, typ_tl, body_tl)
-          | [], [], [] -> []
-          | _ -> assert false
-        in
-        let funs' = combine (funs, types, bodies) in
-        metasenv'', Cic.Fix (i, funs')
-    | Cic.CoFix (i, funs) ->
-        let metasenv', types =
-          List.fold_right
-            (fun (name, typ, _) (metasenv, types) ->
-              let new_metasenv, new_type = aux metasenv context typ in
-              (new_metasenv, (name, new_type) :: types))
-            funs (metasenv, [])
-        in
-        let context' =
-          (List.rev_map
-            (fun (name, t) -> Some (Cic.Name name, Cic.Decl t))
-            types)
-          @ context
-        in
-        let metasenv'', bodies =
-          List.fold_right
-            (fun (_, _, body) (metasenv, bodies) ->
-              let new_metasenv, new_body = aux metasenv context' body in
-              (new_metasenv, new_body :: bodies))
-            funs (metasenv', [])
-        in
-        let rec combine = function
-          | ((name, _, _) :: funs_tl),
-            ((_, typ) :: typ_tl),
-            (body :: body_tl) ->
-              (name, typ, body) :: combine (funs_tl, typ_tl, body_tl)
-          | [], [], [] -> []
-          | _ -> assert false
-        in
-        let funs' = combine (funs, types, bodies) in
-        metasenv'', Cic.CoFix (i, funs')
-  and do_subst metasenv context subst =
-    List.fold_right
-      (fun (uri, term) (metasenv, substs) ->
-        let metasenv', term' = aux metasenv context term in
-        (metasenv', (uri, term') :: substs))
-      subst (metasenv, [])
-  and do_local_context metasenv context local_context =
-    List.fold_right
-      (fun term (metasenv, local_context) ->
-        let metasenv', term' =
-          match term with
-          | None -> metasenv, None
-          | Some term ->
-              let metasenv', term' = aux metasenv context term in
-              metasenv', Some term'
-        in
-        metasenv', term' :: local_context)
-      local_context (metasenv, [])
-  in
-  aux metasenv context term
-
-let expand_implicits_in_obj metasenv subst =
- function
-    Cic.Constant (name,bo,ty,params,attrs) ->
-     let metasenv,bo' =
-      match bo with
-         None -> metasenv,None
-       | Some bo ->
-          let metasenv,bo' = expand_implicits metasenv subst [] bo in
-           metasenv,Some bo' in
-     let metasenv,ty' = expand_implicits metasenv subst [] ty in
-      metasenv,Cic.Constant (name,bo',ty',params,attrs)
-  | Cic.CurrentProof (name,metasenv',bo,ty,params,attrs) ->
-     assert (metasenv' = []);
-     let metasenv,bo' = expand_implicits metasenv subst [] bo in
-     let metasenv,ty' = expand_implicits metasenv subst [] ty in
-      metasenv,Cic.CurrentProof (name,metasenv,bo',ty',params,attrs)
-  | Cic.InductiveDefinition (tyl,params,paramsno,attrs) ->
-     let metasenv,tyl =
-      List.fold_right
-       (fun (name,b,ty,cl) (metasenv,res) ->
-         let metasenv,ty' = expand_implicits metasenv subst [] ty in
-         let metasenv,cl' =
-          List.fold_right
-           (fun (name,ty) (metasenv,res) ->
-             let metasenv,ty' = expand_implicits metasenv subst [] ty in
-              metasenv,(name,ty')::res
-           ) cl (metasenv,[])
-         in
-          metasenv,(name,b,ty',cl')::res
-       ) tyl (metasenv,[])
-     in
-      metasenv,Cic.InductiveDefinition (tyl,params,paramsno,attrs)
-  | Cic.Variable _ -> assert false (* Not implemented *)
index 4f6fcee2e5d917ab06893638597e9e2b150f9839..476270144c9de7cef4b1b3c8512b21ae4f47fcc0 100644 (file)
@@ -58,9 +58,3 @@ val fresh_subst:
         UriManager.uri list -> 
           Cic.metasenv * (Cic.term Cic.explicit_named_substitution)
 
-val expand_implicits:
-  Cic.metasenv -> Cic.substitution -> Cic.context -> Cic.term ->
-    Cic.metasenv * Cic.term
-
-val expand_implicits_in_obj:
-  Cic.metasenv -> Cic.substitution -> Cic.obj -> Cic.metasenv * Cic.obj
index 120fdceaa1b5a08452ff30c4398a0d0cad76bebd..03acb40cb7b7b3c59958b8706a2273b528140bd3 100644 (file)
@@ -50,6 +50,131 @@ let rec split l n =
   | (_,_) -> raise (AssertFailure (lazy "split: list too short"))
 ;;
 
+let exp_impl metasenv subst context term =
+  let rec aux metasenv context = function
+    | (Cic.Rel _) as t -> metasenv, t
+    | (Cic.Sort _) as t -> metasenv, t
+    | Cic.Const (uri, subst) ->
+        let metasenv', subst' = do_subst metasenv context subst in
+        metasenv', Cic.Const (uri, subst')
+    | Cic.Var (uri, subst) ->
+        let metasenv', subst' = do_subst metasenv context subst in
+        metasenv', Cic.Var (uri, subst')
+    | Cic.MutInd (uri, i, subst) ->
+        let metasenv', subst' = do_subst metasenv context subst in
+        metasenv', Cic.MutInd (uri, i, subst')
+    | Cic.MutConstruct (uri, i, j, subst) ->
+        let metasenv', subst' = do_subst metasenv context subst in
+        metasenv', Cic.MutConstruct (uri, i, j, subst')
+    | Cic.Meta (n,l) -> 
+        let metasenv', l' = do_local_context metasenv context l in
+        metasenv', Cic.Meta (n, l')
+    | Cic.Implicit (Some `Type) ->
+        let (metasenv', idx) = CicMkImplicit.mk_implicit_type metasenv subst context in
+        let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
+        metasenv', Cic.Meta (idx, irl)
+    | Cic.Implicit (Some `Closed) ->
+        let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
+        metasenv', Cic.Meta (idx, [])
+    | Cic.Implicit None ->
+        let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
+        let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
+        metasenv', Cic.Meta (idx, irl)
+    | Cic.Implicit _ -> assert false
+    | Cic.Cast (te, ty) ->
+        let metasenv', ty' = aux metasenv context ty in
+        let metasenv'', te' = aux metasenv' context te in
+        metasenv'', Cic.Cast (te', ty')
+    | Cic.Prod (name, s, t) ->
+        let metasenv', s' = aux metasenv context s in
+        metasenv', Cic.Prod (name, s', t)
+    | Cic.Lambda (name, s, t) ->
+        let metasenv', s' = aux metasenv context s in
+        metasenv', Cic.Lambda (name, s', t)
+    | Cic.LetIn (name, s, t) ->
+        let metasenv', s' = aux metasenv context s in
+        metasenv', Cic.LetIn (name, s', t)
+    | Cic.Appl l when List.length l > 1 ->
+        let metasenv', l' =
+          List.fold_right
+            (fun term (metasenv, terms) ->
+              let new_metasenv, term = aux metasenv context term in
+              new_metasenv, term :: terms)
+            l (metasenv, [])
+        in
+        metasenv', Cic.Appl l'
+    | Cic.Appl _ -> assert false
+    | Cic.MutCase (uri, i, outtype, term, patterns) ->
+        let metasenv', l' =
+          List.fold_right
+            (fun term (metasenv, terms) ->
+              let new_metasenv, term = aux metasenv context term in
+              new_metasenv, term :: terms)
+            (outtype :: term :: patterns) (metasenv, [])
+        in
+        let outtype', term', patterns' =
+          match l' with
+          | outtype' :: term' :: patterns' -> outtype', term', patterns'
+          | _ -> assert false
+        in
+        metasenv', Cic.MutCase (uri, i, outtype', term', patterns')
+    | Cic.Fix (i, funs) ->
+        let metasenv', types =
+          List.fold_right
+            (fun (name, _, typ, _) (metasenv, types) ->
+              let new_metasenv, new_type = aux metasenv context typ in
+              (new_metasenv, (name, new_type) :: types))
+            funs (metasenv, [])
+        in
+        let rec combine = function
+          | ((name, index, _, body) :: funs_tl),
+            ((_, typ) :: typ_tl) ->
+              (name, index, typ, body) :: combine (funs_tl, typ_tl)
+          | [], [] -> []
+          | _ -> assert false
+        in
+        let funs' = combine (funs, types) in
+        metasenv', Cic.Fix (i, funs')
+    | Cic.CoFix (i, funs) ->
+        let metasenv', types =
+          List.fold_right
+            (fun (name, typ, _) (metasenv, types) ->
+              let new_metasenv, new_type = aux metasenv context typ in
+              (new_metasenv, (name, new_type) :: types))
+            funs (metasenv, [])
+        in
+        let rec combine = function
+          | ((name, _, body) :: funs_tl),
+            ((_, typ) :: typ_tl) ->
+              (name, typ, body) :: combine (funs_tl, typ_tl)
+          | [], [] -> []
+          | _ -> assert false
+        in
+        let funs' = combine (funs, types) in
+        metasenv', Cic.CoFix (i, funs')
+    | term -> metasenv,term
+  and do_subst metasenv context subst =
+    List.fold_right
+      (fun (uri, term) (metasenv, substs) ->
+        let metasenv', term' = aux metasenv context term in
+        (metasenv', (uri, term') :: substs))
+      subst (metasenv, [])
+  and do_local_context metasenv context local_context =
+    List.fold_right
+      (fun term (metasenv, local_context) ->
+        let metasenv', term' =
+          match term with
+          | None -> metasenv, None
+          | Some term ->
+              let metasenv', term' = aux metasenv context term in
+              metasenv', Some term'
+        in
+        metasenv', term' :: local_context)
+      local_context (metasenv, [])
+  in
+  aux metasenv context term
+;;
+
 let rec type_of_constant uri ugraph =
  let module C = Cic in
  let module R = CicReduction in
@@ -97,7 +222,7 @@ and type_of_mutual_inductive_defs uri i ugraph =
    match obj with
       C.InductiveDefinition (dl,_,_,_) ->
         let (_,_,arity,_) = List.nth dl i in
-        arity,u
+         arity,u
     | _ ->
        raise
         (RefineFailure
@@ -114,14 +239,15 @@ and type_of_mutual_inductive_constr uri i j ugraph =
     with Not_found -> assert false
    in
     match obj with
-       C.InductiveDefinition (dl,_,_,_) ->
-         let (_,_,_,cl) = List.nth dl i in
+        C.InductiveDefinition (dl,_,_,_) ->
+          let (_,_,_,cl) = List.nth dl i in
           let (_,ty) = List.nth cl (j-1) in
             ty,u
-      | _ ->
-         raise
-           (RefineFailure
-               (lazy ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
+      | _ -> 
+          raise
+                  (RefineFailure
+              (lazy 
+                ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
 
 
 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
@@ -139,307 +265,309 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt
     (* let module R = CicMetaSubst in *)
   let module R = CicReduction in
     match R.whd ~subst context expectedtype with
-       C.MutInd (_,_,_) ->
-         (n,context,actualtype, [term]), subst, metasenv, ugraph
+        C.MutInd (_,_,_) ->
+          (n,context,actualtype, [term]), subst, metasenv, ugraph
       | C.Appl (C.MutInd (_,_,_)::tl) ->
-         let (_,arguments) = split tl left_args_no in
-           (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph 
+          let (_,arguments) = split tl left_args_no in
+            (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph 
       | C.Prod (name,so,de) ->
-         (* we expect that the actual type of the branch has the due 
+          (* we expect that the actual type of the branch has the due 
              number of Prod *)
-         (match R.whd ~subst context actualtype with
+          (match R.whd ~subst context actualtype with
                C.Prod (name',so',de') ->
-                let subst, metasenv, ugraph1 = 
-                  fo_unif_subst subst context metasenv so so' ugraph in
-                let term' =
-                  (match CicSubstitution.lift 1 term with
-                       C.Appl l -> C.Appl (l@[C.Rel 1])
+                 let subst, metasenv, ugraph1 = 
+                   fo_unif_subst subst context metasenv so so' ugraph in
+                 let term' =
+                   (match CicSubstitution.lift 1 term with
+                        C.Appl l -> C.Appl (l@[C.Rel 1])
                       | t -> C.Appl [t ; C.Rel 1]) in
-                  (* we should also check that the name variable is anonymous in
-                     the actual type de' ?? *)
-                  check_branch (n+1) 
+                   (* we should also check that the name variable is anonymous in
+                      the actual type de' ?? *)
+                   check_branch (n+1) 
                      ((Some (name,(C.Decl so)))::context) 
                        metasenv subst left_args_no de' term' de ugraph1
              | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
       | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
 
 and type_of_aux' metasenv context t ugraph =
+  let metasenv, t = exp_impl metasenv [] context t in
   let rec type_of_aux subst metasenv context t ugraph =
     let module C = Cic in
     let module S = CicSubstitution in
     let module U = UriManager in
+    (* this stops on binders, so we have to call it every time *)
       match t with
-         (*    function *)
-         C.Rel n ->
-           (try
+          (*    function *)
+          C.Rel n ->
+            (try
                match List.nth context (n - 1) with
-                  Some (_,C.Decl ty) -> 
+                   Some (_,C.Decl ty) -> 
                      t,S.lift n ty,subst,metasenv, ugraph
-                | Some (_,C.Def (_,Some ty)) -> 
+                 | Some (_,C.Def (_,Some ty)) -> 
                      t,S.lift n ty,subst,metasenv, ugraph
-                | Some (_,C.Def (bo,None)) ->
+                 | Some (_,C.Def (bo,None)) ->
                      let ty,ugraph =
                       (* if it is in the context it must be already well-typed*)
-                     CicTypeChecker.type_of_aux' ~subst metasenv context
+                      CicTypeChecker.type_of_aux' ~subst metasenv context
                        (S.lift n bo) ugraph 
                      in
                       t,ty,subst,metasenv,ugraph
-                | None -> raise (RefineFailure (lazy "Rel to hidden hypothesis"))
+                 | None -> raise (RefineFailure (lazy "Rel to hidden hypothesis"))
              with
-                _ -> raise (RefineFailure (lazy "Not a close term"))
-           )
-       | C.Var (uri,exp_named_subst) ->
-           let exp_named_subst',subst',metasenv',ugraph1 =
-             check_exp_named_subst 
+                 _ -> raise (RefineFailure (lazy "Not a close term")))
+        | C.Var (uri,exp_named_subst) ->
+            let exp_named_subst',subst',metasenv',ugraph1 =
+              check_exp_named_subst 
                 subst metasenv context exp_named_subst ugraph 
             in
             let ty_uri,ugraph1 = type_of_variable uri ugraph in
-           let ty =
-             CicSubstitution.subst_vars exp_named_subst' ty_uri
-           in
-             C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
-       | C.Meta (n,l) -> 
+            let ty =
+              CicSubstitution.subst_vars exp_named_subst' ty_uri
+            in
+              C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
+        | C.Meta (n,l) -> 
             (try
                let (canonical_context, term,ty) = 
                  CicUtil.lookup_subst n subst 
                in
                let l',subst',metasenv',ugraph1 =
-                check_metasenv_consistency n subst metasenv context
-                  canonical_context l ugraph 
+                 check_metasenv_consistency n subst metasenv context
+                   canonical_context l ugraph 
                in
-                (* trust or check ??? *)
-                C.Meta (n,l'),CicSubstitution.subst_meta l' ty, 
+                 (* trust or check ??? *)
+                 C.Meta (n,l'),CicSubstitution.subst_meta l' ty, 
                    subst', metasenv', ugraph1
-                  (* type_of_aux subst metasenv 
-                     context (CicSubstitution.subst_meta l term) *)
+                   (* type_of_aux subst metasenv 
+                      context (CicSubstitution.subst_meta l term) *)
              with CicUtil.Subst_not_found _ ->
                let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
                let l',subst',metasenv', ugraph1 =
-                check_metasenv_consistency n subst metasenv context
-                  canonical_context l ugraph
+                 check_metasenv_consistency n subst metasenv context
+                   canonical_context l ugraph
                in
-                C.Meta (n,l'),CicSubstitution.subst_meta l' ty, 
+                 C.Meta (n,l'),CicSubstitution.subst_meta l' ty, 
                    subst', metasenv',ugraph1)
-       | C.Sort (C.Type tno) -> 
+        | C.Sort (C.Type tno) -> 
             let tno' = CicUniv.fresh() in 
-           let ugraph1 = CicUniv.add_gt tno' tno ugraph in
-             t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
-       | C.Sort _ -> 
+            let ugraph1 = CicUniv.add_gt tno' tno ugraph in
+              t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
+        | C.Sort _ -> 
             t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
-       | C.Implicit _ -> raise (AssertFailure (lazy "21"))
-       | C.Cast (te,ty) ->
-           let ty',_,subst',metasenv',ugraph1 =
+        | C.Implicit _ -> raise (AssertFailure (lazy "21"))
+        | C.Cast (te,ty) ->
+            let ty',_,subst',metasenv',ugraph1 =
               type_of_aux subst metasenv context ty ugraph 
             in
-           let te',inferredty,subst'',metasenv'',ugraph2 =
+            let te',inferredty,subst'',metasenv'',ugraph2 =
               type_of_aux subst' metasenv' context te ugraph1
-           in
+            in
               (try
-                let subst''',metasenv''',ugraph3 =
-                  fo_unif_subst subst'' context metasenv'' 
+                 let subst''',metasenv''',ugraph3 =
+                   fo_unif_subst subst'' context metasenv'' 
                      inferredty ty ugraph2
-                in
-                  C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
+                 in
+                   C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
                with
-                  _ -> raise (RefineFailure (lazy "Cast")))
-       | C.Prod (name,s,t) ->
-           let s',sort1,subst',metasenv',ugraph1 = 
+               | _ -> raise (RefineFailure (lazy "Cast")))
+        | C.Prod (name,s,t) ->
+            let carr t subst context = CicMetaSubst.apply_subst subst t in
+            let coerce_to_sort 
+              in_source tgt_sort t type_to_coerce subst ctx metasenv uragph 
+            =
+              let coercion_src = carr type_to_coerce subst ctx in
+              match coercion_src with
+              | Cic.Sort _ -> 
+                  t,type_to_coerce,subst,metasenv,ugraph
+(*
+              | Cic.Meta _ as meta when not in_source -> 
+                  let coercion_tgt = carr (Cic.Sort tgt_sort) subst ctx in
+                  let subst, metasenv, ugraph = 
+                    fo_unif_subst 
+                      subst ctx metasenv meta coercion_tgt ugraph
+                  in
+                  t, Cic.Sort tgt_sort, subst, metasenv, ugraph
+*)
+              | Cic.Meta _ as meta -> 
+                  t, meta, subst, metasenv, ugraph
+              | Cic.Cast _ as cast -> 
+                  t, cast, subst, metasenv, ugraph
+              | term -> 
+                  let coercion_tgt = carr (Cic.Sort tgt_sort) subst ctx in
+                  let search = CoercGraph.look_for_coercion in
+                  let boh = search coercion_src coercion_tgt in
+                  (match boh with
+                  | CoercGraph.NoCoercion ->
+                      raise (RefineFailure (lazy "no coercion"))
+                  | CoercGraph.NotHandled _ -> 
+                      raise (RefineFailure (lazy "not a sort in PI"))
+                  | CoercGraph.NotMetaClosed -> 
+                      raise (Uncertain (lazy "Coercions on metas 1"))
+                  | CoercGraph.SomeCoercion c -> 
+                      Cic.Appl [c;t],Cic.Sort tgt_sort,subst, metasenv, ugraph)
+            in
+            let s',sort1,subst',metasenv',ugraph1 = 
               type_of_aux subst metasenv context s ugraph 
             in
-           let t',sort2,subst'',metasenv'',ugraph2 =
+            let s',sort1,subst', metasenv',ugraph1 = 
+              coerce_to_sort true (Cic.Type(CicUniv.fresh()))
+              s' sort1 subst' context metasenv' ugraph1
+            in
+            let context_for_t = ((Some (name,(C.Decl s')))::context) in
+            let metasenv',t = exp_impl metasenv' subst' context_for_t t in
+            let t',sort2,subst'',metasenv'',ugraph2 =
               type_of_aux subst' metasenv' 
-                ((Some (name,(C.Decl s')))::context) t ugraph1
-           in
-            (try
+                context_for_t t ugraph1
+            in
+            let t',sort2,subst'',metasenv'',ugraph2 = 
+              coerce_to_sort false (Cic.Type(CicUniv.fresh()))
+              t' sort2 subst'' context_for_t metasenv'' ugraph2
+            in
               let sop,subst''',metasenv''',ugraph3 =
                 sort_of_prod subst'' metasenv'' 
                   context (name,s') (sort1,sort2) ugraph2
               in
                 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
-            with
-            | RefineFailure _ as exn ->
-                (* given [t] of type [type_to_coerce] returns
-                 * a term that has type [tgt_sort] eventually 
-                 * derived from (coercion [t]) *)
-                let refined_target = t' in
-                let sort_of_refined_target = sort2 in
-                let carr t subst context = CicMetaSubst.apply_subst subst t in
-                let coerce_to_sort tgt_sort t type_to_coerce subst ctx =
-                  match type_to_coerce with
-                  | Cic.Sort _ -> t
-                  | term -> 
-                      let coercion_src = carr type_to_coerce subst ctx in
-                      let coercion_tgt = carr (Cic.Sort tgt_sort) subst ctx in
-                      let search = CoercGraph.look_for_coercion in
-                      (match search coercion_src coercion_tgt with
-                      | CoercGraph.NoCoercion 
-                      | CoercGraph.NotHandled _ -> raise exn
-                      | CoercGraph.NotMetaClosed -> 
-                          raise (Uncertain (lazy "Coercions on metas"))
-                      | CoercGraph.SomeCoercion c -> Cic.Appl [c;t])
-                in
-                (* this is probably not the best... *)
-                let tgt_sort_for_pi_source = Cic.Type(CicUniv.fresh()) in
-                let tgt_sort_for_pi_target = Cic.Type(CicUniv.fresh()) in
-                let new_src = 
-                  coerce_to_sort tgt_sort_for_pi_source s sort1 subst context 
-                in
-                let context_with_new_src = 
-                  ((Some (name,(C.Decl new_src)))::context) 
-                in
-                let new_tgt = 
-                  coerce_to_sort 
-                    tgt_sort_for_pi_target 
-                    refined_target sort_of_refined_target
-                    subst context_with_new_src
-                in
-                let newprod = C.Prod (name,new_src,new_tgt) in
-                let _,sort_of_refined_prod,subst,metasenv,ugraph3 =
-                  type_of_aux subst metasenv context newprod ugraph2
-                in
-                (* this if for a coercion on the tail of the arrow *)
-                let new_target = 
-                  match sort_of_refined_target with
-                  | Cic.Sort _ -> refined_target
-                  | _ -> new_tgt
-                in
-                C.Prod(name,new_src,new_target),
-                sort_of_refined_prod,subst,metasenv,ugraph3) 
-       | C.Lambda (n,s,t) ->
-           let s',sort1,subst',metasenv',ugraph1 = 
-             type_of_aux subst metasenv context s ugraph
-           in
-             (match CicReduction.whd ~subst:subst' context sort1 with
-                  C.Meta _
-                | C.Sort _ -> ()
-                | _ ->
-                    raise (RefineFailure (lazy (sprintf
-                                            "Not well-typed lambda-abstraction: the source %s should be a type;
-             instead it is a term of type %s" (CicPp.ppterm s)
-                                            (CicPp.ppterm sort1))))
-             ) ;
-             let t',type2,subst'',metasenv'',ugraph2 =
-               type_of_aux subst' metasenv' 
-                  ((Some (n,(C.Decl s')))::context) t ugraph1
-             in
-               C.Lambda (n,s',t'),C.Prod (n,s',type2),
-                  subst'',metasenv'',ugraph2
-       | C.LetIn (n,s,t) ->
-           (* only to check if s is well-typed *)
-           let s',ty,subst',metasenv',ugraph1 = 
-             type_of_aux subst metasenv context s ugraph
-           in
-           let t',inferredty,subst'',metasenv'',ugraph2 =
-             type_of_aux subst' metasenv' 
-                ((Some (n,(C.Def (s',Some ty))))::context) t ugraph1
-           in
-             (* One-step LetIn reduction. 
+        | C.Lambda (n,s,t) ->
+
+            let s',sort1,subst',metasenv',ugraph1 = 
+              type_of_aux subst metasenv context s ugraph
+            in
+            (match CicReduction.whd ~subst:subst' context sort1 with
+                 C.Meta _
+               | C.Sort _ -> ()
+               | _ ->
+                   raise (RefineFailure (lazy (sprintf
+                                           "Not well-typed lambda-abstraction: the source %s should be a type;
+           instead it is a term of type %s" (CicPp.ppterm s)
+                                           (CicPp.ppterm sort1))))
+            ) ;
+            let context_for_t = ((Some (n,(C.Decl s')))::context) in 
+            let metasenv',t = exp_impl metasenv' subst' context_for_t t in
+            let t',type2,subst'',metasenv'',ugraph2 =
+              type_of_aux subst' metasenv' 
+                context_for_t t ugraph1
+            in
+              C.Lambda (n,s',t'),C.Prod (n,s',type2),
+                subst'',metasenv'',ugraph2
+        | C.LetIn (n,s,t) ->
+            (* only to check if s is well-typed *)
+            let s',ty,subst',metasenv',ugraph1 = 
+              type_of_aux subst metasenv context s ugraph
+            in
+           let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
+            let metasenv',t = exp_impl metasenv' subst' context_for_t t in
+           
+            let t',inferredty,subst'',metasenv'',ugraph2 =
+              type_of_aux subst' metasenv' 
+                context_for_t t ugraph1
+            in
+              (* One-step LetIn reduction. 
                * Even faster than the previous solution.
-              * Moreover the inferred type is closer to the expected one. 
+               * Moreover the inferred type is closer to the expected one. 
                *)
-             C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
+              C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
                 subst'',metasenv'',ugraph2
-       | C.Appl (he::((_::_) as tl)) ->
-           let he',hetype,subst',metasenv',ugraph1 = 
-             type_of_aux subst metasenv context he ugraph 
-           in
-           let tlbody_and_type,subst'',metasenv'',ugraph2 =
-             List.fold_right
-               (fun x (res,subst,metasenv,ugraph) ->
-                  let x',ty,subst',metasenv',ugraph1 =
-                    type_of_aux subst metasenv context x ugraph
-                  in
-                    (x', ty)::res,subst',metasenv',ugraph1
-               ) tl ([],subst',metasenv',ugraph1)
-           in
+        | C.Appl (he::((_::_) as tl)) ->
+            let he',hetype,subst',metasenv',ugraph1 = 
+              type_of_aux subst metasenv context he ugraph 
+            in
+            let tlbody_and_type,subst'',metasenv'',ugraph2 =
+              List.fold_right
+                (fun x (res,subst,metasenv,ugraph) ->
+                   let x',ty,subst',metasenv',ugraph1 =
+                     type_of_aux subst metasenv context x ugraph
+                   in
+                     (x', ty)::res,subst',metasenv',ugraph1
+                ) tl ([],subst',metasenv',ugraph1)
+            in
             let tl',applty,subst''',metasenv''',ugraph3 =
-             eat_prods subst'' metasenv'' context 
+              eat_prods subst'' metasenv'' context 
                 hetype tlbody_and_type ugraph2
             in
               C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3
-       | C.Appl _ -> raise (RefineFailure (lazy "Appl: no arguments"))
-       | C.Const (uri,exp_named_subst) ->
-           let exp_named_subst',subst',metasenv',ugraph1 =
-             check_exp_named_subst subst metasenv context 
+        | C.Appl _ -> raise (RefineFailure (lazy "Appl: no arguments"))
+        | C.Const (uri,exp_named_subst) ->
+            let exp_named_subst',subst',metasenv',ugraph1 =
+              check_exp_named_subst subst metasenv context 
                 exp_named_subst ugraph in
-           let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
-           let cty =
-             CicSubstitution.subst_vars exp_named_subst' ty_uri
-           in
-             C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
-       | C.MutInd (uri,i,exp_named_subst) ->
-           let exp_named_subst',subst',metasenv',ugraph1 =
-             check_exp_named_subst subst metasenv context 
+            let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
+            let cty =
+              CicSubstitution.subst_vars exp_named_subst' ty_uri
+            in
+              C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
+        | C.MutInd (uri,i,exp_named_subst) ->
+            let exp_named_subst',subst',metasenv',ugraph1 =
+              check_exp_named_subst subst metasenv context 
                 exp_named_subst ugraph 
-           in
-           let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
-           let cty =
-             CicSubstitution.subst_vars exp_named_subst' ty_uri in
-             C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
-       | C.MutConstruct (uri,i,j,exp_named_subst) ->
-           let exp_named_subst',subst',metasenv',ugraph1 =
-             check_exp_named_subst subst metasenv context 
+            in
+            let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
+            let cty =
+              CicSubstitution.subst_vars exp_named_subst' ty_uri in
+              C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
+        | C.MutConstruct (uri,i,j,exp_named_subst) ->
+            let exp_named_subst',subst',metasenv',ugraph1 =
+              check_exp_named_subst subst metasenv context 
                 exp_named_subst ugraph 
             in
-           let ty_uri,ugraph2 = 
+            let ty_uri,ugraph2 = 
               type_of_mutual_inductive_constr uri i j ugraph1 
             in
-           let cty =
-             CicSubstitution.subst_vars exp_named_subst' ty_uri 
+            let cty =
+              CicSubstitution.subst_vars exp_named_subst' ty_uri 
             in
-             C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
+              C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
                 metasenv',ugraph2
-       | C.MutCase (uri, i, outtype, term, pl) ->
-           (* first, get the inductive type (and noparams) 
+        | C.MutCase (uri, i, outtype, term, pl) ->
+            (* first, get the inductive type (and noparams) 
              * in the environment  *)
-           let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
+            let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
               let _ = CicTypeChecker.typecheck uri in
-             let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
+              let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
               match obj with
-                 C.InductiveDefinition (l,expl_params,parsno,_) -> 
-                   List.nth l i , expl_params, parsno, u
-               | _ ->
-                   raise
-                     (RefineFailure
-                        (lazy ("Unkown mutual inductive definition " ^ 
+                  C.InductiveDefinition (l,expl_params,parsno,_) -> 
+                    List.nth l i , expl_params, parsno, u
+                | _ ->
+                    raise
+                      (RefineFailure
+                         (lazy ("Unkown mutual inductive definition " ^ 
                          U.string_of_uri uri)))
            in
-          let rec count_prod t =
+           let rec count_prod t =
              match CicReduction.whd ~subst context t with
-                C.Prod (_, _, t) -> 1 + (count_prod t)
-              | _ -> 0 
+                 C.Prod (_, _, t) -> 1 + (count_prod t)
+               | _ -> 0 
            in 
-          let no_args = count_prod arity in
-            (* now, create a "generic" MutInd *)
-          let metasenv,left_args = 
+           let no_args = count_prod arity in
+             (* now, create a "generic" MutInd *)
+           let metasenv,left_args = 
              CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
            in
-          let metasenv,right_args = 
+           let metasenv,right_args = 
              let no_right_params = no_args - no_left_params in
-              if no_right_params < 0 then assert false
-              else CicMkImplicit.n_fresh_metas 
+               if no_right_params < 0 then assert false
+               else CicMkImplicit.n_fresh_metas 
                       metasenv subst context no_right_params 
            in
-          let metasenv,exp_named_subst = 
+           let metasenv,exp_named_subst = 
              CicMkImplicit.fresh_subst metasenv subst context expl_params in
-          let expected_type = 
+           let expected_type = 
              if no_args = 0 then 
-              C.MutInd (uri,i,exp_named_subst)
+               C.MutInd (uri,i,exp_named_subst)
              else
-              C.Appl 
+               C.Appl 
                  (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
-          in
-            (* check consistency with the actual type of term *)
-          let term',actual_type,subst,metasenv,ugraph1 = 
+           in
+             (* check consistency with the actual type of term *)
+           let term',actual_type,subst,metasenv,ugraph1 = 
              type_of_aux subst metasenv context term ugraph in
-          let expected_type',_, subst, metasenv,ugraph2 =
+           let expected_type',_, subst, metasenv,ugraph2 =
              type_of_aux subst metasenv context expected_type ugraph1
-          in
-          let actual_type = CicReduction.whd ~subst context actual_type in
-          let subst,metasenv,ugraph3 =
+           in
+           let actual_type = CicReduction.whd ~subst context actual_type in
+           let subst,metasenv,ugraph3 =
              fo_unif_subst subst context metasenv 
                expected_type' actual_type ugraph2
-          in
+           in
            let rec instantiate_prod t =
             function
                [] -> t
@@ -451,37 +579,37 @@ and type_of_aux' metasenv context t ugraph =
            in
            let arity_instantiated_with_left_args =
             instantiate_prod arity left_args in
-            (* TODO: check if the sort elimination 
+             (* TODO: check if the sort elimination 
               * is allowed: [(I q1 ... qr)|B] *)
-          let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
+           let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
              List.fold_left
-              (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
-                 let constructor =
-                   if left_args = [] then
-                     (C.MutConstruct (uri,i,j,exp_named_subst))
-                   else
-                     (C.Appl 
+               (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
+                  let constructor =
+                    if left_args = [] then
+                      (C.MutConstruct (uri,i,j,exp_named_subst))
+                    else
+                      (C.Appl 
                         (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
-                 in
-                 let p',actual_type,subst,metasenv,ugraph1 = 
-                   type_of_aux subst metasenv context p ugraph 
                   in
-                 let constructor',expected_type, subst, metasenv,ugraph2 = 
-                   type_of_aux subst metasenv context constructor ugraph1 
+                  let p',actual_type,subst,metasenv,ugraph1 = 
+                    type_of_aux subst metasenv context p ugraph 
                   in
-                 let outtypeinstance,subst,metasenv,ugraph3 =
-                   check_branch 0 context metasenv subst no_left_params 
+                  let constructor',expected_type, subst, metasenv,ugraph2 = 
+                    type_of_aux subst metasenv context constructor ugraph1 
+                  in
+                  let outtypeinstance,subst,metasenv,ugraph3 =
+                    check_branch 0 context metasenv subst no_left_params 
                       actual_type constructor' expected_type ugraph2 
                   in
-                   (pl @ [p'],j+1,
+                    (pl @ [p'],j+1,
                      outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
-              ([],1,[],subst,metasenv,ugraph3) pl 
+               ([],1,[],subst,metasenv,ugraph3) pl 
            in
            
              (* we are left to check that the outype matches his instances.
-               The easy case is when the outype is specified, that amount
-               to a trivial check. Otherwise, we should guess a type from
-               its instances 
+                The easy case is when the outype is specified, that amount
+                to a trivial check. Otherwise, we should guess a type from
+                its instances 
              *)
              
            (match outtype with
@@ -541,7 +669,7 @@ and type_of_aux' metasenv context t ugraph =
                      let metasenv,new_meta = 
                        CicMkImplicit.mk_implicit metasenv subst extended_context
                      in
-                    let irl =
+                       let irl =
                        CicMkImplicit.identity_relocation_list_for_metavariable 
                          extended_context
                      in
@@ -642,33 +770,34 @@ and type_of_aux' metasenv context t ugraph =
                   (CicMetaSubst.apply_subst subst
                    (C.Appl(outtype::right_args@[term]))),
                  subst,metasenv,ugraph6)
-       | C.Fix (i,fl) ->
-           let fl_ty',subst,metasenv,types,ugraph1 =
-             List.fold_left
-               (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
-                  let ty',_,subst',metasenv',ugraph1 = 
+        | C.Fix (i,fl) ->
+            let fl_ty',subst,metasenv,types,ugraph1 =
+              List.fold_left
+                (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
+                   let ty',_,subst',metasenv',ugraph1 = 
                       type_of_aux subst metasenv context ty ugraph 
                    in
-                    fl @ [ty'],subst',metasenv', 
+                     fl @ [ty'],subst',metasenv', 
                        Some (C.Name n,(C.Decl ty')) :: types, ugraph
-               ) ([],subst,metasenv,[],ugraph) fl
-           in
-           let len = List.length types in
-           let context' = types@context in
-           let fl_bo',subst,metasenv,ugraph2 =
+                ) ([],subst,metasenv,[],ugraph) fl
+            in
+            let len = List.length types in
+            let context' = types@context in
+            let fl_bo',subst,metasenv,ugraph2 =
               List.fold_left
-               (fun (fl,subst,metasenv,ugraph) (name,x,ty,bo) ->
-                  let bo',ty_of_bo,subst,metasenv,ugraph1 =
-                    type_of_aux subst metasenv context' bo ugraph
-                  in
+                (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
+                   let metasenv, bo = exp_impl metasenv subst context' bo in
+                   let bo',ty_of_bo,subst,metasenv,ugraph1 =
+                     type_of_aux subst metasenv context' bo ugraph
+                   in
                    let subst',metasenv',ugraph' =
-                    fo_unif_subst subst context' metasenv
-                      ty_of_bo (CicSubstitution.lift len ty) ugraph1
+                     fo_unif_subst subst context' metasenv
+                       ty_of_bo (CicSubstitution.lift len ty) ugraph1
                    in 
                      fl @ [bo'] , subst',metasenv',ugraph'
-               ) ([],subst,metasenv,ugraph1) fl 
+                ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty') 
             in
-            let (_,_,ty,_) = List.nth fl i in
+            let ty = List.nth fl_ty' i in
             (* now we have the new ty in fl_ty', the new bo in fl_bo',
              * and we want the new fl with bo' and ty' injected in the right
              * place.
@@ -683,33 +812,34 @@ and type_of_aux' metasenv context t ugraph =
               fl_ty' fl_bo' fl 
             in
               C.Fix (i,fl''),ty,subst,metasenv,ugraph2
-       | C.CoFix (i,fl) ->
-           let fl_ty',subst,metasenv,types,ugraph1 =
-             List.fold_left
-               (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
-                  let ty',_,subst',metasenv',ugraph1 = 
+        | C.CoFix (i,fl) ->
+            let fl_ty',subst,metasenv,types,ugraph1 =
+              List.fold_left
+                (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
+                   let ty',_,subst',metasenv',ugraph1 = 
                      type_of_aux subst metasenv context ty ugraph 
                    in
-                    fl @ [ty'],subst',metasenv', 
+                     fl @ [ty'],subst',metasenv', 
                        Some (C.Name n,(C.Decl ty')) :: types, ugraph1
-               ) ([],subst,metasenv,[],ugraph) fl
-           in
-           let len = List.length types in
-           let context' = types@context in
-           let fl_bo',subst,metasenv,ugraph2 =
+                ) ([],subst,metasenv,[],ugraph) fl
+            in
+            let len = List.length types in
+            let context' = types@context in
+            let fl_bo',subst,metasenv,ugraph2 =
               List.fold_left
-               (fun (fl,subst,metasenv,ugraph) (name,ty,bo) ->
-                  let bo',ty_of_bo,subst,metasenv,ugraph1 =
-                    type_of_aux subst metasenv context' bo ugraph
-                  in
+                (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
+                   let metasenv, bo = exp_impl metasenv subst context' bo in
+                   let bo',ty_of_bo,subst,metasenv,ugraph1 =
+                     type_of_aux subst metasenv context' bo ugraph
+                   in
                    let subst',metasenv',ugraph' = 
-                    fo_unif_subst subst context' metasenv
+                     fo_unif_subst subst context' metasenv
                        ty_of_bo (CicSubstitution.lift len ty) ugraph1
                    in
                      fl @ [bo'],subst',metasenv',ugraph'
-               ) ([],subst,metasenv,ugraph1) fl 
+                ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
             in
-            let (_,ty,_) = List.nth fl i in
+            let ty = List.nth fl_ty' i in
             (* now we have the new ty in fl_ty', the new bo in fl_bo',
              * and we want the new fl with bo' and ty' injected in the right
              * place.
@@ -736,92 +866,88 @@ and type_of_aux' metasenv context t ugraph =
     let module S = CicSubstitution in
     let lifted_canonical_context = 
       let rec aux i =
-       function
+        function
             [] -> []
-         | (Some (n,C.Decl t))::tl ->
+          | (Some (n,C.Decl t))::tl ->
               (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
-         | (Some (n,C.Def (t,None)))::tl ->
+          | (Some (n,C.Def (t,None)))::tl ->
               (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
-         | None::tl -> None::(aux (i+1) tl)
-         | (Some (n,C.Def (t,Some ty)))::tl ->
+          | None::tl -> None::(aux (i+1) tl)
+          | (Some (n,C.Def (t,Some ty)))::tl ->
               (Some (n,
-                    C.Def ((S.subst_meta l (S.lift i t)),
-                           Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
+                     C.Def ((S.subst_meta l (S.lift i t)),
+                            Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
       in
-       aux 1 canonical_context 
+        aux 1 canonical_context 
     in
       try
-       List.fold_left2 
-         (fun (l,subst,metasenv,ugraph) t ct -> 
+        List.fold_left2 
+          (fun (l,subst,metasenv,ugraph) t ct -> 
              match (t,ct) with
-                _,None ->
-                  l @ [None],subst,metasenv,ugraph
+                 _,None ->
+                   l @ [None],subst,metasenv,ugraph
                | Some t,Some (_,C.Def (ct,_)) ->
                    let subst',metasenv',ugraph' = 
-                  (try
-                     fo_unif_subst subst context metasenv t ct ugraph
-                   with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
+                   (try
+                      fo_unif_subst subst context metasenv t ct ugraph
+                    with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
                    in
                      l @ [Some t],subst',metasenv',ugraph'
                | Some t,Some (_,C.Decl ct) ->
-                  let t',inferredty,subst',metasenv',ugraph1 =
-                    type_of_aux subst metasenv context t ugraph
-                  in
+                   let t',inferredty,subst',metasenv',ugraph1 =
+                     type_of_aux subst metasenv context t ugraph
+                   in
                    let subst'',metasenv'',ugraph2 = 
-                    (try
-                       fo_unif_subst
-                         subst' context metasenv' inferredty ct ugraph1
-                     with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
+                     (try
+                        fo_unif_subst
+                          subst' context metasenv' inferredty ct ugraph1
+                      with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with AssertFailure msg -> Lazy.force msg | RefineFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
                    in
                      l @ [Some t'], subst'',metasenv'',ugraph2
                | None, Some _  ->
-                  raise (RefineFailure (lazy (sprintf
-                                          "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s"
-                                          (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
-                                          (CicMetaSubst.ppcontext subst canonical_context))))
-         ) ([],subst,metasenv,ugraph) l lifted_canonical_context 
+                   raise (RefineFailure (lazy (sprintf "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s" (CicMetaSubst.ppterm subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext subst canonical_context))))) ([],subst,metasenv,ugraph) l lifted_canonical_context 
       with
-         Invalid_argument _ ->
-           raise
-           (RefineFailure
+          Invalid_argument _ ->
+            raise
+            (RefineFailure
                (lazy (sprintf
-                 "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
-                 (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
-                 (CicMetaSubst.ppcontext subst canonical_context))))
+                  "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
+                  (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
+                  (CicMetaSubst.ppcontext subst canonical_context))))
 
   and check_exp_named_subst metasubst metasenv context tl ugraph =
     let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph  =
       match tl with
-         [] -> [],metasubst,metasenv,ugraph
-       | ((uri,t) as subst)::tl ->
-           let ty_uri,ugraph1 =  type_of_variable uri ugraph in
-           let typeofvar =
+          [] -> [],metasubst,metasenv,ugraph
+        | ((uri,t) as subst)::tl ->
+            let ty_uri,ugraph1 =  type_of_variable uri ugraph in
+            let typeofvar =
               CicSubstitution.subst_vars substs ty_uri in
-             (* CSC: why was this code here? it is wrong
-                (match CicEnvironment.get_cooked_obj ~trust:false uri with
-                Cic.Variable (_,Some bo,_,_) ->
-                raise
-                (RefineFailure (Reason
-                "A variable with a body can not be explicit substituted"))
-                | Cic.Variable (_,None,_,_) -> ()
-                | _ ->
-                raise
-                (RefineFailure (Reason
-                ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
-                ) ;
-             *)
-           let t',typeoft,metasubst',metasenv',ugraph2 =
+              (* CSC: why was this code here? it is wrong
+                 (match CicEnvironment.get_cooked_obj ~trust:false uri with
+                 Cic.Variable (_,Some bo,_,_) ->
+                 raise
+                 (RefineFailure (lazy
+                 "A variable with a body can not be explicit substituted"))
+                 | Cic.Variable (_,None,_,_) -> ()
+                 | _ ->
+                 raise
+                 (RefineFailure (lazy
+                 ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
+                 ) ;
+              *)
+            let t',typeoft,metasubst',metasenv',ugraph2 =
               type_of_aux metasubst metasenv context t ugraph1
-           in
+            in
             let metasubst'',metasenv'',ugraph3 =
               try
-               fo_unif_subst 
+                fo_unif_subst 
                   metasubst' context metasenv' typeoft typeofvar ugraph2
               with _ ->
-               raise (RefineFailure (lazy
-                        ("Wrong Explicit Named Substitution: " ^ 
+                raise (RefineFailure (lazy
+                         ("Wrong Explicit Named Substitution: " ^ 
                            CicMetaSubst.ppterm metasubst' typeoft ^
-                         " not unifiable with " ^ 
+                          " not unifiable with " ^ 
                           CicMetaSubst.ppterm metasubst' typeofvar)))
             in
             (* FIXME: no mere tail recursive! *)
@@ -840,19 +966,19 @@ and type_of_aux' metasenv context t ugraph =
     let t1'' = CicReduction.whd ~subst context t1 in
     let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
       match (t1'', t2'') with
-         (C.Sort s1, C.Sort s2)
+          (C.Sort s1, C.Sort s2)
             when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> 
               (* different than Coq manual!!! *)
               C.Sort s2,subst,metasenv,ugraph
-       | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> 
-           let t' = CicUniv.fresh() in 
-           let ugraph1 = CicUniv.add_ge t' t1 ugraph in
-           let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
-             C.Sort (C.Type t'),subst,metasenv,ugraph2
-       | (C.Sort _,C.Sort (C.Type t1)) -> 
-           C.Sort (C.Type t1),subst,metasenv,ugraph
-       | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
-       | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
+        | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> 
+            let t' = CicUniv.fresh() in 
+            let ugraph1 = CicUniv.add_ge t' t1 ugraph in
+            let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
+              C.Sort (C.Type t'),subst,metasenv,ugraph2
+        | (C.Sort _,C.Sort (C.Type t1)) -> 
+            C.Sort (C.Type t1),subst,metasenv,ugraph
+        | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
+        | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
             (* TODO how can we force the meta to become a sort? If we don't we
              * brake the invariant that refine produce only well typed terms *)
             (* TODO if we check the non meta term and if it is a sort then we
@@ -878,71 +1004,71 @@ and type_of_aux' metasenv context t ugraph =
   and eat_prods subst metasenv context hetype tlbody_and_type ugraph =
     let rec mk_prod metasenv context =
       function
-         [] ->
-           let (metasenv, idx) = 
+          [] ->
+            let (metasenv, idx) = 
               CicMkImplicit.mk_implicit_type metasenv subst context 
             in
-           let irl =
+            let irl =
               CicMkImplicit.identity_relocation_list_for_metavariable context
-           in
+            in
               metasenv,Cic.Meta (idx, irl)
-       | (_,argty)::tl ->
-           let (metasenv, idx) = 
+        | (_,argty)::tl ->
+            let (metasenv, idx) = 
               CicMkImplicit.mk_implicit_type metasenv subst context 
             in
-           let irl =
-             CicMkImplicit.identity_relocation_list_for_metavariable context
-           in
-           let meta = Cic.Meta (idx,irl) in
-           let name =
+            let irl =
+              CicMkImplicit.identity_relocation_list_for_metavariable context
+            in
+            let meta = Cic.Meta (idx,irl) in
+            let name =
               (* The name must be fresh for context.                 *)
               (* Nevertheless, argty is well-typed only in context.  *)
               (* Thus I generate a name (name_hint) in context and   *)
               (* then I generate a name --- using the hint name_hint *)
               (* --- that is fresh in (context'@context).            *)
               let name_hint = 
-               (* Cic.Name "pippo" *)
-               FreshNamesGenerator.mk_fresh_name ~subst metasenv 
-                 (*           (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
-                 (CicMetaSubst.apply_subst_context subst context)
-                 Cic.Anonymous
-                 ~typ:(CicMetaSubst.apply_subst subst argty) 
+                (* Cic.Name "pippo" *)
+                FreshNamesGenerator.mk_fresh_name ~subst metasenv 
+                  (*           (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
+                  (CicMetaSubst.apply_subst_context subst context)
+                  Cic.Anonymous
+                  ~typ:(CicMetaSubst.apply_subst subst argty) 
               in
-               (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
-               FreshNamesGenerator.mk_fresh_name ~subst
-                 [] context name_hint ~typ:(Cic.Sort Cic.Prop)
-           in
-           let metasenv,target =
+                (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
+                FreshNamesGenerator.mk_fresh_name ~subst
+                  [] context name_hint ~typ:(Cic.Sort Cic.Prop)
+            in
+            let metasenv,target =
               mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
-           in
+            in
               metasenv,Cic.Prod (name,meta,target)
     in
     let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
     let (subst, metasenv,ugraph1) =
       try
-       fo_unif_subst subst context metasenv hetype hetype' ugraph
+        fo_unif_subst subst context metasenv hetype hetype' ugraph
       with exn ->
-       debug_print (lazy (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
-                        (CicPp.ppterm hetype)
-                        (CicPp.ppterm hetype')
+        debug_print (lazy (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
+                         (CicPp.ppterm hetype)
+                         (CicPp.ppterm hetype')
                          (CicMetaSubst.ppmetasenv [] metasenv)
-                        (CicMetaSubst.ppsubst subst)));
-       raise exn
+                         (CicMetaSubst.ppsubst subst)));
+        raise exn
 
     in
     let rec eat_prods metasenv subst context hetype ugraph =
       function
         | [] -> [],metasenv,subst,hetype,ugraph
-       | (hete, hety)::tl ->
+        | (hete, hety)::tl ->
             (match hetype with
-                Cic.Prod (n,s,t) ->
-                  let arg,subst,metasenv,ugraph1 =
-                    try
+                 Cic.Prod (n,s,t) ->
+                   let arg,subst,metasenv,ugraph1 =
+                     try
                        let subst,metasenv,ugraph1 = 
                          fo_unif_subst subst context metasenv hety s ugraph
                        in
                          hete,subst,metasenv,ugraph1
-                    with exn ->
+                     with exn ->
                        (* we search a coercion from hety to s *)
                        let coer = 
                          let carr t subst context = 
@@ -959,9 +1085,9 @@ and type_of_aux' metasenv context t ugraph =
                            raise (Uncertain (lazy "Coercions on meta"))
                        | CoercGraph.SomeCoercion c -> 
                            (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph
-                  in
+                   in
                    let coerced_args,metasenv',subst',t',ugraph2 =
-                    eat_prods metasenv subst context
+                     eat_prods metasenv subst context
                        (* (CicMetaSubst.subst subst hete t) tl *)
                        (CicSubstitution.subst hete t) ugraph1 tl
                    in
@@ -1001,18 +1127,18 @@ and type_of_aux' metasenv context t ugraph =
          let context' =
            List.map
              (function
-                 None -> None
-               | Some (n, Cic.Decl t) ->
-                   Some (n,
-                         Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
-               | Some (n, Cic.Def (bo,ty)) ->
-                   let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
-                   let ty' =
+                  None -> None
+                | Some (n, Cic.Decl t) ->
+                    Some (n,
+                          Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
+                | Some (n, Cic.Def (bo,ty)) ->
+                    let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
+                    let ty' =
                       match ty with
-                         None -> None
-                       | Some ty ->
-                           Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
-                   in
+                          None -> None
+                        | Some ty ->
+                            Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
+                    in
                       Some (n, Cic.Def (bo',ty'))
              ) context
          in
@@ -1028,17 +1154,80 @@ let type_of_aux' metasenv context term ugraph =
   with 
     CicUniv.UniverseInconsistency msg -> raise (RefineFailure (lazy msg))
 
-(*CSC: this is a very very rough approximation; to be finished *)
-let are_all_occurrences_positive uri =
- let rec aux =
-  (*CSC: here we should do a whd; but can we do that? *)
-  function
-     Cic.Appl (Cic.MutInd (uri',_,_)::_) when uri = uri' -> ()
-   | Cic.MutInd (uri',_,_) when uri = uri' -> ()
-   | Cic.Prod (_,_,t) -> aux t
-   | _ -> raise (RefineFailure (lazy "not well formed constructor type"))
- in
-  aux
+let undebrujin uri typesno tys t =
+  snd
+   (List.fold_right
+     (fun (name,_,_,_) (i,t) ->
+       (* here the explicit_named_substituion is assumed to be *)
+       (* of length 0 *)
+       let t' = Cic.MutInd (uri,i,[])  in
+       let t = CicSubstitution.subst t' t in
+        i - 1,t
+     ) tys (typesno - 1,t)) 
+
+let map_first_n n start f g l = 
+  let rec aux acc k l =
+    if k < n then
+      match l with
+      | [] -> raise (Invalid_argument "map_first_n")
+      | hd :: tl -> f hd k (aux acc (k+1) tl)
+    else
+      g acc l
+  in
+  aux start 0 l
+   
+(*CSC: this is a very rough approximation; to be finished *)
+let are_all_occurrences_positive metasenv ugraph uri tys leftno =
+  let number_of_types = List.length tys in
+  let subst,metasenv,ugraph,tys = 
+    List.fold_right
+      (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
+        let subst,metasenv,ugraph,cl = 
+          List.fold_right
+            (fun (name,ty) (subst,metasenv,ugraph,acc) ->
+               let rec aux ctx k subst = function
+                 | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
+                     let subst,metasenv,ugraph,tl = 
+                       map_first_n leftno 
+                         (subst,metasenv,ugraph,[]) 
+                         (fun t n (subst,metasenv,ugraph,acc) ->
+                           let subst,metasenv,ugraph = 
+                             fo_unif_subst 
+                               subst ctx metasenv t (Cic.Rel (k-n)) ugraph 
+                           in
+                           subst,metasenv,ugraph,(t::acc)) 
+                         (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl)) 
+                         tl
+                     in
+                     subst,metasenv,ugraph,(Cic.Appl (hd::tl))
+                 | Cic.MutInd(uri',_,_) as t when uri = uri'->
+                     subst,metasenv,ugraph,t 
+                 | Cic.Prod (name,s,t) -> 
+                     let ctx = (Some (name,Cic.Decl s))::ctx in 
+                     let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
+                     subst,metasenv,ugraph,Cic.Prod (name,s,t)
+                 | _ -> 
+                     raise 
+                      (RefineFailure 
+                        (lazy "not well formed constructor type"))
+               in
+               let subst,metasenv,ugraph,ty = aux [] 0 subst ty in  
+               subst,metasenv,ugraph,(name,ty) :: acc)
+          cl (subst,metasenv,ugraph,[])
+        in 
+        subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
+      tys ([],metasenv,ugraph,[])
+  in
+  let substituted_tys = 
+    List.map 
+      (fun (name,ind,arity,cl) -> 
+        let cl = 
+          List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
+        in
+        name,ind,CicMetaSubst.apply_subst subst arity,cl)
+      tys 
+  in
+  metasenv,ugraph,substituted_tys
     
 let typecheck metasenv uri obj =
  let ugraph = CicUniv.empty_ugraph in
@@ -1098,27 +1287,16 @@ let typecheck metasenv uri obj =
              let ty = CicTypeChecker.debrujin_constructor uri typesno ty in
              let ty',_,metasenv,ugraph =
               type_of_aux' metasenv con_context ty ugraph in
-             let undebrujin t =
-              snd
-               (List.fold_right
-                 (fun (name,_,_,_) (i,t) ->
-                   (* here the explicit_named_substituion is assumed to be *)
-                   (* of length 0 *)
-                   let t' = Cic.MutInd (uri,i,[])  in
-                   let t = CicSubstitution.subst t' t in
-                    i - 1,t
-                 ) tys (typesno - 1,t)) in
-             let ty' = undebrujin ty' in
+             let ty' = undebrujin uri typesno tys ty' in
               metasenv,ugraph,(name,ty')::res
            ) cl (metasenv,ugraph,[])
          in
           metasenv,ugraph,(name,b,ty,cl')::res
        ) tys (metasenv,ugraph,[]) in
      (* third phase: we check the positivity condition *)
-     List.iter
-      (fun (_,_,_,cl) ->
-        List.iter (fun (_,ty) -> are_all_occurrences_positive uri ty) cl
-      ) tys ;
+     let metasenv,ugraph,tys = 
+       are_all_occurrences_positive metasenv ugraph uri tys paramsno 
+     in
      Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
 
 (* DEBUGGING ONLY