COERCIONS: tentative addition of an equivalence relation over coercion source

[helm.git] / components / cic_unification / cicRefine.ml

diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index 840a955cb8a7218749b74aeed1203ab52485004f..856c9a58622480d6f938cbeb0e8a25c1ce913473 100644 (file)
--- a/components/cic_unification/cicRefine.ml
+++ b/components/cic_unification/cicRefine.ml
@@ -454,6 +454,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                     in
                     (match boh with
                     | CoercGraph.NoCoercion
+                    | CoercGraph.SomeCoercionToTgt _
                     | CoercGraph.NotHandled _ ->
                        enrich localization_tbl t
                         (RefineFailure 
@@ -526,6 +527,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                      in
                       match boh with
                       | CoercGraph.NoCoercion
+                      | CoercGraph.SomeCoercionToTgt _
                       |  CoercGraph.NotHandled _ ->
                         enrich localization_tbl s'
                          (RefineFailure 
@@ -1363,6 +1365,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
         | CoercGraph.NoCoercion 
         | CoercGraph.NotMetaClosed 
         | CoercGraph.NotHandled _ -> raise exn
+        | CoercGraph.SomeCoercionToTgt candidates
         | CoercGraph.SomeCoercion candidates ->
             match  
             HExtlib.list_findopt 
@@ -1447,6 +1450,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                     in
                     (match coer with
                     | CoercGraph.NoCoercion 
+                    | CoercGraph.SomeCoercionToTgt _
                     | CoercGraph.NotHandled _ ->
                         enrich localization_tbl hete exn
                          ~f:(fun _ ->