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 d6504eb1584c28c5ec7abd5ff4d190e1daa7135b..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 
@@ -677,8 +679,6 @@ 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 
@@ -1365,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 
@@ -1449,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 _ ->