many printings added

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 120fed3ebde9a4c3f2b8142e9ab651136fcb1f41..1490417f1f30306daf85f33c55136371b1e773e9 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -78,8 +78,10 @@ let enrich localization_tbl t ?(f = fun msg -> msg) exn =
   match exn with
      RefineFailure msg -> RefineFailure (f msg)
    | Uncertain msg -> Uncertain (f msg)
+   | AssertFailure msg -> prerr_endline (Lazy.force msg); AssertFailure (f msg)
    | Sys.Break -> raise exn
-   | _ -> assert false in
+   | _ -> prerr_endline (Printexc.to_string exn); assert false 
+ in
  let loc =
   try
    Cic.CicHash.find localization_tbl t
@@ -422,7 +424,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                exn ->
                 enrich localization_tbl te'
                  ~f:(fun _ ->
-                   lazy ("The term " ^
+                   lazy ("(3)The term " ^
                     CicMetaSubst.ppterm_in_context metasenv'' subst'' te'
                      context ^ " has type " ^
                     CicMetaSubst.ppterm_in_context metasenv'' subst'' inferredty
@@ -455,7 +457,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                     | CoercGraph.NotHandled _ ->
                        enrich localization_tbl t
                         (RefineFailure 
-                          (lazy ("The term " ^ 
+                          (lazy ("(4)The term " ^ 
                           CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ 
                           " is not a type since it has type " ^ 
                           CicMetaSubst.ppterm_in_context ~metasenv
@@ -463,7 +465,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                     | CoercGraph.NotMetaClosed -> 
                        enrich localization_tbl t
                         (Uncertain 
-                          (lazy ("The term " ^ 
+                          (lazy ("(5)The term " ^ 
                           CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ 
                           " is not a type since it has type " ^ 
                           CicMetaSubst.ppterm_in_context ~metasenv
@@ -479,7 +481,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                         | None -> 
                             enrich localization_tbl t
                               (RefineFailure 
-                                (lazy ("The term " ^ 
+                                (lazy ("(6)The term " ^ 
                                 CicMetaSubst.ppterm_in_context ~metasenv
                                   subst t context ^ 
                                   " is not a type since it has type " ^ 
@@ -527,7 +529,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                       |  CoercGraph.NotHandled _ ->
                         enrich localization_tbl s'
                          (RefineFailure 
-                          (lazy ("The term " ^ 
+                          (lazy ("(7)The term " ^ 
                           CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^ 
                           " is not a type since it has type " ^ 
                           CicMetaSubst.ppterm_in_context ~metasenv
@@ -535,7 +537,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                       | CoercGraph.NotMetaClosed -> 
                         enrich localization_tbl s'
                          (Uncertain 
-                          (lazy ("The term " ^ 
+                          (lazy ("(8)The term " ^ 
                           CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^ 
                           " is not a type since it has type " ^ 
                           CicMetaSubst.ppterm_in_context ~metasenv 
@@ -551,7 +553,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                         | None -> 
                            enrich localization_tbl s'
                             (RefineFailure 
-                             (lazy ("The term " ^ 
+                             (lazy ("(9)The term " ^ 
                               CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^ 
                               " is not a type since it has type " ^ 
                               CicMetaSubst.ppterm_in_context ~metasenv
@@ -675,15 +677,19 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
              type_of_aux subst metasenv context expected_type ugraph1
            in
            let actual_type = CicReduction.whd ~subst context actual_type in
+           prerr_endline (CicPp.ppterm expected_type');
+           prerr_endline (CicPp.ppterm actual_type);
            let subst,metasenv,ugraph3 =
             try
              fo_unif_subst subst context metasenv 
                expected_type' actual_type ugraph2
             with
              exn ->
+               prerr_endline (CicMetaSubst.ppmetasenv subst metasenv);
+               prerr_endline (CicMetaSubst.ppsubst subst ~metasenv);
               enrich localization_tbl term' exn
                ~f:(function _ ->
-                 lazy ("The term " ^
+                 lazy ("(10)The term " ^
                   CicMetaSubst.ppterm_in_context ~metasenv subst term'
                    context ^ " has type " ^
                   CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
@@ -728,7 +734,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                     exn ->
                      enrich localization_tbl constructor'
                       ~f:(fun _ ->
-                        lazy ("The term " ^
+                        lazy ("(11)The term " ^
                          CicMetaSubst.ppterm_in_context metasenv subst p'
                           context ^ " has type " ^
                          CicMetaSubst.ppterm_in_context metasenv subst actual_type
@@ -916,7 +922,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                       exn ->
                        enrich localization_tbl p exn
                         ~f:(function _ ->
-                          lazy ("The term " ^
+                          lazy ("(12)The term " ^
                            CicMetaSubst.ppterm_in_context ~metasenv subst p
                             context ^ " has type " ^
                            CicMetaSubst.ppterm_in_context ~metasenv subst instance'
@@ -957,7 +963,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                      exn ->
                       enrich localization_tbl bo exn
                        ~f:(function _ ->
-                         lazy ("The term " ^
+                         lazy ("(13)The term " ^
                           CicMetaSubst.ppterm_in_context ~metasenv subst bo
                            context' ^ " has type " ^
                           CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
@@ -1010,7 +1016,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                      exn ->
                       enrich localization_tbl bo exn
                        ~f:(function _ ->
-                         lazy ("The term " ^
+                         lazy ("(14)The term " ^
                           CicMetaSubst.ppterm_in_context ~metasenv subst bo
                            context' ^ " has type " ^
                           CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
@@ -1446,7 +1452,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                     | CoercGraph.NotHandled _ ->
                         enrich localization_tbl hete exn
                          ~f:(fun _ ->
-                           (lazy ("The term " ^
+                           (lazy ("(15)The term " ^
                              CicMetaSubst.ppterm_in_context ~metasenv subst hete
                               context ^ " has type " ^
                              CicMetaSubst.ppterm_in_context ~metasenv subst hety
@@ -1456,7 +1462,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                     | CoercGraph.NotMetaClosed -> 
                         enrich localization_tbl hete exn
                          ~f:(fun _ ->
-                           (lazy ("The term " ^
+                           (lazy ("(16)The term " ^
                              CicMetaSubst.ppterm_in_context ~metasenv subst hete
                               context ^ " has type " ^
                              CicMetaSubst.ppterm_in_context ~metasenv subst hety
@@ -1492,7 +1498,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                         | None ->  
                            enrich localization_tbl hete
                             ~f:(fun _ ->
-                             (lazy ("The term " ^
+                             (lazy ("(1)The term " ^
                               CicMetaSubst.ppterm_in_context ~metasenv subst hete
                                context ^ " has type " ^
                               CicMetaSubst.ppterm_in_context ~metasenv subst hety
@@ -1502,7 +1508,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                   | exn ->
                      enrich localization_tbl hete
                       ~f:(fun _ ->
-                        (lazy ("The term " ^
+                        (lazy ("(2)The term " ^
                           CicMetaSubst.ppterm_in_context ~metasenv subst hete
                            context ^ " has type " ^
                           CicMetaSubst.ppterm_in_context ~metasenv subst hety