From c80afcec268c6b6037c039f00b97274483632843 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 28 Apr 2005 13:31:37 +0000
Subject: [PATCH] deactivated coercions

---
 helm/ocaml/cic_unification/cicRefine.ml | 3 +++
 1 file changed, 3 insertions(+)

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
+  *)
 ;;
 
 
-- 
2.39.2