X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_unification%2FcicRefine.ml;h=120fed3ebde9a4c3f2b8142e9ab651136fcb1f41;hb=590854ef49fa6c6ce12a4e3cd2b480266b62f589;hp=9cb0a04a43b8c5c55c34a224248e078f73f8f9ce;hpb=001b43beae9e912a921da426d23c1e437328bb9e;p=helm.git

diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index 9cb0a04a4..120fed3eb 100644
--- a/components/cic_unification/cicRefine.ml
+++ b/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 =
@@ -705,8 +704,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
              (* TODO: check if the sort elimination 
               * is allowed: [(I q1 ... qr)|B] *)
            let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
-             List.fold_left
-               (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
+             List.fold_right
+               (fun p (pl,j,outtypeinstances,subst,metasenv,ugraph) ->
                   let constructor =
                     if left_args = [] then
                       (C.MutConstruct (uri,i,j,exp_named_subst))
@@ -721,12 +720,25 @@ 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
-                    (pl @ [p'],j+1,
-                     outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
-               ([],1,[],subst,metasenv,ugraph3) pl 
+                    (p'::pl,j-1,
+                     outtypeinstances@[outtypeinstance],subst,metasenv,ugraph3))
+               pl ([],List.length pl,[],subst,metasenv,ugraph3)
            in
            
              (* we are left to check that the outype matches his instances.
@@ -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