diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-02 22:58:48 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-02 22:58:48 +0000 |
| commit | 4318eefacae280fed3a159acfede35c568b2942b (patch) | |
| tree | fcbec538a568a7cc75af45fec579e121f84e2c77 /pretyping | |
| parent | 8404c8cd83aa8c802b628afe0c222b87bc7956ef (diff) | |
Modifs suite à intégration de class.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@192 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rwxr-xr-x | pretyping/classops.ml | 12 | ||||
| -rw-r--r-- | pretyping/classops.mli | 4 |
2 files changed, 13 insertions, 3 deletions
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 |