added support for coercions

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

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index eda04d36e33dcd68e54c5eefffee5e8b0ce2f355..1e655b35248dc36ca2f3d32939c76bdf5087c709 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -833,9 +833,9 @@ and type_of_aux' metasenv context t ugraph =
                          hete,subst,metasenv,ugraph1
                     with exn ->
                        (* we search a coercion from hety to s *)
-                       let coer = None (* CoercGraph.look_for_coercion  
+                       let coer = CoercGraph.look_for_coercion 
                          (CicMetaSubst.apply_subst subst hety) 
-                         (CicMetaSubst.apply_subst subst s) *)
+                         (CicMetaSubst.apply_subst subst s) 
                        in
                        match coer with
                        | None -> raise exn