X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=120fed3ebde9a4c3f2b8142e9ab651136fcb1f41;hb=a95bb53a77f84592a64131eadf7d4501c49667ce;hp=6d26a868b10e956267954ccfe1b9d0029d08f235;hpb=c5f2c1c89032b6b65499de04af9f2b7428059c67;p=helm.git

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 6d26a868b..120fed3eb 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -509,7 +509,6 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
               in
                 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
         | C.Lambda (n,s,t) ->
-
             let s',sort1,subst',metasenv',ugraph1 = 
               type_of_aux subst metasenv context s ugraph in
             let s',sort1,subst',metasenv',ugraph1 =
@@ -721,8 +720,21 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                     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 
+                   try
+                    check_branch 0 context metasenv subst
+                     no_left_params actual_type constructor' expected_type
+                     ugraph2 
+                   with
+                    exn ->
+                     enrich localization_tbl constructor'
+                      ~f:(fun _ ->
+                        lazy ("The term " ^
+                         CicMetaSubst.ppterm_in_context metasenv subst p'
+                          context ^ " has type " ^
+                         CicMetaSubst.ppterm_in_context metasenv subst actual_type
+                          context ^ " but is here used with type " ^
+                         CicMetaSubst.ppterm_in_context metasenv subst expected_type
+                          context)) exn
                   in
                     (p'::pl,j-1,
                      outtypeinstances@[outtypeinstance],subst,metasenv,ugraph3))
@@ -919,17 +931,17 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                    (C.Appl(outtype::right_args@[term]))),
                  subst,metasenv,ugraph6)
         | C.Fix (i,fl) ->
-            let fl_ty',subst,metasenv,types,ugraph1 =
+            let fl_ty',subst,metasenv,types,ugraph1,len =
               List.fold_left
-                (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
+                (fun (fl,subst,metasenv,types,ugraph,len) (n,_,ty,_) ->
                    let ty',_,subst',metasenv',ugraph1 = 
                       type_of_aux subst metasenv context ty ugraph 
                    in
                      fl @ [ty'],subst',metasenv', 
-                       Some (C.Name n,(C.Decl ty')) :: types, ugraph
-                ) ([],subst,metasenv,[],ugraph) fl
+                       Some (C.Name n,(C.Decl (CicSubstitution.lift len ty')))
+                        :: types, ugraph, len+1
+                ) ([],subst,metasenv,[],ugraph,0) fl
             in
-            let len = List.length types in
             let context' = types@context in
             let fl_bo',subst,metasenv,ugraph2 =
               List.fold_left
@@ -972,17 +984,17 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
             in
               C.Fix (i,fl''),ty,subst,metasenv,ugraph2
         | C.CoFix (i,fl) ->
-            let fl_ty',subst,metasenv,types,ugraph1 =
+            let fl_ty',subst,metasenv,types,ugraph1,len =
               List.fold_left
-                (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
+                (fun (fl,subst,metasenv,types,ugraph,len) (n,ty,_) ->
                    let ty',_,subst',metasenv',ugraph1 = 
                      type_of_aux subst metasenv context ty ugraph 
                    in
                      fl @ [ty'],subst',metasenv', 
-                       Some (C.Name n,(C.Decl ty')) :: types, ugraph1
-                ) ([],subst,metasenv,[],ugraph) fl
+                      Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) ::
+                        types, ugraph1, len+1
+                ) ([],subst,metasenv,[],ugraph,0) fl
             in
-            let len = List.length types in
             let context' = types@context in
             let fl_bo',subst,metasenv,ugraph2 =
               List.fold_left