Serious bug fixed: the types of a real mutual fix definition were not lifted

as required. Moreover, an unification exception used to escape the refiner.
Now it does no more, but the error is not localized (being about the branch
of a MutCase that has no precise localization).

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 6d26a868b10e956267954ccfe1b9d0029d08f235..120fed3ebde9a4c3f2b8142e9ab651136fcb1f41 100644 (file)
--- 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