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 1490417f1f30306daf85f33c55136371b1e773e9..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 _ ->
@@ -1734,6 +1736,7 @@ let typecheck metasenv uri obj ~localization_tbl =
      let con_context =
       List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
      (* second phase: we fix only the constructors *)
+     let saved_menv = metasenv in
      let metasenv,ugraph,tys =
       List.fold_right
        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
@@ -1746,7 +1749,7 @@ let typecheck metasenv uri obj ~localization_tbl =
              let ty',_,metasenv,ugraph =
               type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
              let ty' = undebrujin uri typesno tys ty' in
-              metasenv,ugraph,(name,ty')::res
+              metasenv@saved_menv,ugraph,(name,ty')::res
            ) cl (metasenv,ugraph,[])
          in
           metasenv,ugraph,(name,b,ty,cl')::res