X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=dd5191a156543b59148d15ff261938f7548425e2;hb=18d8d7128c16b5d4dd589d75a2e7c026ac7d405d;hp=318d1e742be3aa5e4daf0436574e04a9d8d87b5c;hpb=c4f53600c65b71ae9e213a54bade36c0c2e2ae37;p=helm.git

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 318d1e742..dd5191a15 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -337,15 +337,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                match List.nth context (n - 1) with
                    Some (_,C.Decl ty) -> 
                      t,S.lift n ty,subst,metasenv, ugraph
-                 | Some (_,C.Def (_,Some ty)) -> 
+                 | Some (_,C.Def (_,ty)) -> 
                      t,S.lift n ty,subst,metasenv, ugraph
-                 | 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
-                       (S.lift n bo) ugraph 
-                     in
-                      t,ty,subst,metasenv,ugraph
                  | None ->
                     enrich localization_tbl t
                      (RefineFailure (lazy "Rel to hidden hypothesis"))
@@ -445,12 +438,29 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
             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
+        | C.LetIn (n,s,ty,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 ty,_,subst',metasenv',ugraph1 =
+             type_of_aux subst' metasenv' context ty ugraph1 in
+           let subst',metasenv',ugraph1 =
+            try
+             fo_unif_subst subst' context metasenv'
+               ty ty' ugraph1
+            with
+             exn ->
+              enrich localization_tbl s' exn
+               ~f:(function _ ->
+                 lazy ("The term " ^
+                  CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' s'
+                   context ^ " has type " ^
+                  CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty'
+                   context ^ " but is here used with type " ^
+                  CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty
+                   context))
+           in
+           let context_for_t = ((Some (n,(C.Def (s',ty))))::context) in
            
             let t',inferredty,subst'',metasenv'',ugraph2 =
               type_of_aux subst' metasenv' 
@@ -460,7 +470,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                * Even faster than the previous solution.
                * Moreover the inferred type is closer to the expected one. 
                *)
-              C.LetIn (n,s',t'),
+              C.LetIn (n,s',ty,t'),
                CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
                subst'',metasenv'',ugraph2
         | C.Appl (he::((_::_) as tl)) ->
@@ -939,13 +949,13 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
             [] -> []
           | (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 ((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 ->
-              (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)
+          | (Some (n,C.Def (t,ty)))::tl ->
+              (Some
+               (n,
+                C.Def
+                 (S.subst_meta l (S.lift i t),
+                  S.subst_meta l (S.lift i ty)))) :: (aux (i+1) tl)
       in
         aux 1 canonical_context 
     in
@@ -1751,11 +1761,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                           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)
+                    let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty
                     in
                       Some (n, Cic.Def (bo',ty'))
              ) context
@@ -1972,13 +1978,11 @@ let pack_coercion metasenv ctx t =
    | C.Lambda (name,so,dest) -> 
        let ctx' = (Some (name,C.Decl so))::ctx in
        C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
-   | C.LetIn (name,so,dest) -> 
-       let _,ty,metasenv,ugraph =
-        pack_coercions := false;
-        type_of_aux' metasenv ctx so CicUniv.oblivion_ugraph in
-        pack_coercions := true;
-       let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in
-       C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
+   | C.LetIn (name,so,ty,dest) -> 
+       let ctx' = Some (name,(C.Def (so,ty)))::ctx in
+       C.LetIn
+        (name, merge_coercions ctx so, merge_coercions ctx ty,
+         merge_coercions ctx' dest)
    | C.Appl l -> 
       let l = List.map (merge_coercions ctx) l in
       let t = C.Appl l in