Bug fixed: an unification exception used to escape when coercions were disabled.

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 49c85a72eea1b0fc09efb2d805f988040f12d4e4..d52b8aa7c66b77d041c1ba5b151e9e9606b84044 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -568,7 +568,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
              exn ->
               enrich localization_tbl term' exn
                ~f:(function _ ->
-                 lazy ("(10)The term " ^
+                 lazy ("The term " ^
                   CicMetaSubst.ppterm_in_context ~metasenv subst term'
                    context ^ " has type " ^
                   CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
@@ -613,7 +613,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                     exn ->
                      enrich localization_tbl constructor'
                       ~f:(fun _ ->
-                        lazy ("(11)The term " ^
+                        lazy ("The term " ^
                          CicMetaSubst.ppterm_in_context metasenv subst p'
                           context ^ " has type " ^
                          CicMetaSubst.ppterm_in_context metasenv subst actual_type
@@ -800,7 +800,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                       exn ->
                        enrich localization_tbl p exn
                         ~f:(function _ ->
-                          lazy ("(12)The term " ^
+                          lazy ("The term " ^
                            CicMetaSubst.ppterm_in_context ~metasenv subst p
                             context ^ " has type " ^
                            CicMetaSubst.ppterm_in_context ~metasenv subst instance'
@@ -841,7 +841,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                      exn ->
                       enrich localization_tbl bo exn
                        ~f:(function _ ->
-                         lazy ("(13)The term " ^
+                         lazy ("The term " ^
                           CicMetaSubst.ppterm_in_context ~metasenv subst bo
                            context' ^ " has type " ^
                           CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
@@ -894,7 +894,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                      exn ->
                       enrich localization_tbl bo exn
                        ~f:(function _ ->
-                         lazy ("(14)The term " ^
+                         lazy ("The term " ^
                           CicMetaSubst.ppterm_in_context ~metasenv subst bo
                            context' ^ " has type " ^
                           CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
@@ -1373,10 +1373,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
           fo_unif_subst subst context metasenv infty expty ugraph
         in
         (t, expty), subst, metasenv, ugraph
-      with Uncertain _ | RefineFailure _ as exn ->
-        if not allow_coercions || not !insert_coercions then
-          enrich localization_tbl t exn
-        else
+      with (Uncertain _ | RefineFailure _ as exn)
+        when allow_coercions && !insert_coercions ->
           let whd = CicReduction.whd ~delta:false in
           let clean t s c = whd c (CicMetaSubst.apply_subst s t) in
           let infty = clean infty subst context in