diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-01 23:13:01 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-01 23:13:01 +0000 |
| commit | f99150300603ce0d87db716efc52fa88967d4460 (patch) | |
| tree | 4a85be13031030ac01659359b032411bfd63a73b /pretyping/classops.mli | |
| parent | 3a49dbf016e1ebf8f8d12ed43fde14c5619ca55e (diff) | |
Intégration du Termast et du Retyping de HH, et modifications connexes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@185 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/classops.mli')
| -rw-r--r-- | pretyping/classops.mli | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 8c2f84887..709b26b85 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -43,7 +43,9 @@ type inheritance_path = int list val cte_of_constr : constr -> cte_typ val class_info : cl_typ -> (int * cl_info_typ) +val class_info_from_index : int -> cl_typ * cl_info_typ 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 val class_of : env -> 'c evar_map -> constr -> constr * int val class_args_of : constr -> constr list @@ -55,10 +57,6 @@ val lookup_path_between : (int * int) -> inheritance_path val lookup_path_to_fun_from : int -> inheritance_path val lookup_path_to_sort_from : int -> inheritance_path val coe_value : int -> (unsafe_judgment * bool) -val print_graph : unit -> (int * string) Pp.ppcmd_token Stream.t -val print_classes : unit -> (int * string) Pp.ppcmd_token Stream.t -val print_coercions : unit -> (int * string) Pp.ppcmd_token Stream.t -val print_path_between : identifier -> identifier -> (int * string) ppcmd_token Stream.t val arity_sort : constr -> int val fully_applied : identifier -> int -> int -> unit val stre_of_cl : cl_typ -> strength |