]> matita.cs.unibo.it Git - helm.git/commitdiff
Bug fixed: the source and target of declared parametric coercions used to
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 18 Feb 2006 19:31:28 +0000 (19:31 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 18 Feb 2006 19:31:28 +0000 (19:31 +0000)
be URIs of the inductive block instead of being URIs of single inductive
types or constructors.

helm/software/components/library/coercDb.ml

index 7203f3647e6eefb642c5fd93be6ff7d465918aa5..c5356b3e17fb2dfe1f4722b22b4a952643bf9464 100644 (file)
@@ -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