From 4318eefacae280fed3a159acfede35c568b2942b Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 2 Dec 1999 22:58:48 +0000
Subject: Modifs suite à intégration de class.ml
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@192 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/classops.ml  | 12 ++++++++++--
 pretyping/classops.mli |  4 +++-
 2 files changed, 13 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index b8a95a0bc..d21e1ba81 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -16,13 +16,13 @@ open Generic
 type cte_typ = 
   | NAM_Var of identifier 
   | NAM_SP of section_path 
-  | NAM_Construct of section_path*int*int
+  | NAM_Construct of constructor_path
 
 let cte_of_constr = function  
   | DOPN(Const sp,_) -> NAM_SP sp
   | DOPN(MutInd (sp,_),_) -> NAM_SP sp
   | VAR id -> NAM_Var id
-  | DOPN(MutConstruct ((sp,i),j) ,_) -> NAM_Construct (sp,i,j)
+  | DOPN(MutConstruct cstr_cp,_) -> NAM_Construct cstr_cp
   |  _ -> raise Not_found
 
 type cl_typ = 
@@ -119,6 +119,10 @@ let search_info x l =
 
 let class_info cl = search_info cl (!cLASSES)
 
+let class_exists cl =
+  try let _ = class_info cl in true
+  with Not_found -> false
+
 (* class_info_from_index : int -> cl_typ * cl_info_typ *)
 
 let class_info_from_index i = List.assoc i (!cLASSES)
@@ -127,6 +131,10 @@ let class_info_from_index i = List.assoc i (!cLASSES)
 
 let coercion_info coe = search_info coe (!cOERCIONS)
 
+let coercion_exists coe =
+  try let _ = coercion_info coe in true
+  with Not_found -> false
+
 (* coercion_info_from_index : int -> coe_typ * coe_info_typ *)
 
 let coercion_info_from_index i = 
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 26188c853..a4bf0ee8f 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -26,7 +26,7 @@ type cl_info_typ = {
 type cte_typ = 
   | NAM_Var of identifier 
   | NAM_SP of section_path 
-  | NAM_Construct of section_path * int * int
+  | NAM_Construct of constructor_path
 
 type coe_typ = cte_typ
 
@@ -45,7 +45,9 @@ val coercions : unit -> (int * (coe_typ * coe_info_typ)) list
 
 val cte_of_constr : constr -> cte_typ
 val class_info : cl_typ -> (int * cl_info_typ)
+val class_exists : cl_typ -> bool
 val class_info_from_index : int -> cl_typ * cl_info_typ
+val coercion_exists : coe_typ -> bool
 val coercion_info : coe_typ -> (int * coe_info_typ)
 val coercion_info_from_index : int -> coe_typ * coe_info_typ
 val constructor_at_head : constr -> cl_typ * int
-- 
cgit v1.2.3