1. The last commit that fixed unification of compound coercions with

[helm.git] / helm / ocaml / library / coercDb.ml

diff --git a/helm/ocaml/library/coercDb.ml b/helm/ocaml/library/coercDb.ml
index 01065325f8c7d5ef729cfcd34540773463aef2cd..8e2c62f310ca5b14251dcaa0a72dd2f94424688e 100644 (file)
--- a/helm/ocaml/library/coercDb.ml
+++ b/helm/ocaml/library/coercDb.ml
@@ -37,9 +37,21 @@ let coerc_carr_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
 ;;
 
+let name_of_carr = function
+  | Uri u -> UriManager.name_of_uri u
+  | Sort s -> CicPp.ppsort s
+  | Term (Cic.Appl ((Cic.Const (uri, _))::_)) 
+  | Term (Cic.Appl ((Cic.MutInd (uri, _, _))::_)) 
+  | Term (Cic.Appl ((Cic.MutConstruct (uri, _, _, _))::_)) -> 
+        UriManager.name_of_uri uri
+  | Term t -> (* CicPp.ppterm t *) assert false
+
 let eq_carr src tgt =
   match src, tgt with
   | Uri src, Uri tgt -> UriManager.eq src tgt
@@ -54,12 +66,6 @@ let eq_carr src tgt =
     else raise EqCarrOnNonMetaClosed
   | _, _ -> false
 
-let name_of_carr = function
-  | Uri u -> UriManager.name_of_uri u
-  | Sort s -> CicPp.ppsort s
-  | Term t -> CicPp.ppterm t
-  
-
 let to_list () =
   !db