From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 26 Jan 2009 17:10:31 +0000 (+0000)
Subject: added a number to identical error messages to ease tracing them
X-Git-Tag: make_still_working~4234
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=24898ae10160660dac8d13fda33d90d3b1f4ace6;p=helm.git

added a number to identical error messages to ease tracing them
---

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index eb350d2e5..40eaa1ba6 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -505,7 +505,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
              exn ->
               enrich localization_tbl s' exn
                ~f:(function _ ->
-                 lazy ("The term " ^
+                 lazy ("(2) The term " ^
                   CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' s'
                    context ^ " has type " ^
                   CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty'
@@ -631,7 +631,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
              exn ->
               enrich localization_tbl term' exn
                ~f:(function _ ->
-                 lazy ("The term " ^
+                 lazy ("(3) The term " ^
                   CicMetaSubst.ppterm_in_context ~metasenv subst term'
                    context ^ " has type " ^
                   CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
@@ -677,7 +677,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                     exn ->
                      enrich localization_tbl constructor'
                       ~f:(fun _ ->
-                        lazy ("The term " ^
+                        lazy ("(4) The term " ^
                          CicMetaSubst.ppterm_in_context metasenv subst p'
                           context ^ " has type " ^
                          CicMetaSubst.ppterm_in_context metasenv subst actual_type
@@ -865,7 +865,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                       exn ->
                        enrich localization_tbl p exn
                         ~f:(function _ ->
-                          lazy ("The term " ^
+                          lazy ("(5) The term " ^
                            CicMetaSubst.ppterm_in_context ~metasenv subst p
                             context ^ " has type " ^
                            CicMetaSubst.ppterm_in_context ~metasenv subst instance'
@@ -906,7 +906,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                      exn ->
                       enrich localization_tbl bo exn
                        ~f:(function _ ->
-                         lazy ("The term " ^
+                         lazy ("(7) The term " ^
                           CicMetaSubst.ppterm_in_context ~metasenv subst bo
                            context' ^ " has type " ^
                           CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
@@ -959,7 +959,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                      exn ->
                       enrich localization_tbl bo exn
                        ~f:(function _ ->
-                         lazy ("The term " ^
+                         lazy ("(8) The term " ^
                           CicMetaSubst.ppterm_in_context ~metasenv subst bo
                            context' ^ " has type " ^
                           CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
@@ -1790,7 +1790,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
       coerce_to_something_aux t infty expty subst metasenv context ugraph
     with Uncertain _ | RefineFailure _ as exn ->
       let f _ =
-        lazy ("The term " ^
+        lazy ("(9) The term " ^
           CicMetaSubst.ppterm_in_context metasenv subst t context ^ 
           " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst
           infty context ^ " but is here used with type " ^ 
@@ -1973,7 +1973,7 @@ let typecheck metasenv uri obj ~localization_tbl =
          RefineFailure _
        | Uncertain _ as exn ->
           let msg = 
-            lazy ("The term " ^
+            lazy ("(1) The term " ^
              CicMetaSubst.ppterm_in_context ~metasenv [] bo' [] ^
              " has type " ^
              CicMetaSubst.ppterm_in_context ~metasenv [] boty [] ^