From 28e4648362227bf701b19b01a23163f9480c62bd Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 18 Feb 2006 19:31:28 +0000 Subject: [PATCH] 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. --- helm/software/components/library/coercDb.ml | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) 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 -- 2.39.2