From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 18 Feb 2006 19:31:28 +0000 (+0000)
Subject: Bug fixed: the source and target of declared parametric coercions used to
X-Git-Tag: make_still_working~7554
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=28e4648362227bf701b19b01a23163f9480c62bd;p=helm.git

Bug fixed: the source and target of declared parametric coercions used to
be URIs of the inductive block instead of being URIs of single inductive
types or constructors.
---

diff --git a/helm/software/components/library/coercDb.ml b/helm/software/components/library/coercDb.ml
index 7203f3647..c5356b3e1 100644
--- a/helm/software/components/library/coercDb.ml
+++ b/helm/software/components/library/coercDb.ml
@@ -32,15 +32,13 @@ exception EqCarrOnNonMetaClosed
 let db = ref []
 
 let coerc_carr_of_term t =
-  try
-    Uri (CicUtil.uri_of_term t)
-  with Invalid_argument _ ->
-    match t with
-    | Cic.Sort s -> Sort s
-    | Cic.Appl ((Cic.Const (uri, _))::_) 
-    | Cic.Appl ((Cic.MutInd (uri, _, _))::_) 
-    | Cic.Appl ((Cic.MutConstruct (uri, _, _, _))::_) -> Uri uri
-    | t -> Term t
+ try
+  match t with
+     Cic.Sort s -> Sort s
+   | Cic.Appl (t::_)
+   | t -> Uri (CicUtil.uri_of_term t)
+ with Invalid_argument _ ->
+  Term t
 ;;
 
 let rec name_of_carr = function