From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 28 Apr 2005 13:31:37 +0000 (+0000)
Subject: deactivated coercions
X-Git-Tag: single_binding~145
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c80afcec268c6b6037c039f00b97274483632843;p=helm.git

deactivated coercions
---

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 621834e33..c5f775253 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -47,6 +47,8 @@ let rec split l n =
 ;;
 
 let look_for_coercion src tgt =
+  None
+  (*
   if (src = (CicUtil.term_of_uri "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)")) &&
      (tgt = (CicUtil.term_of_uri "cic:/Coq/Reals/Rdefinitions/R.con")) 
   then
@@ -60,6 +62,7 @@ let look_for_coercion src tgt =
       (CicPp.ppterm tgt));
     None
     end
+  *)
 ;;