diff options
Diffstat (limited to 'toplevel/class.mli')
| -rw-r--r-- | toplevel/class.mli | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/toplevel/class.mli b/toplevel/class.mli new file mode 100644 index 000000000..094b2ecc2 --- /dev/null +++ b/toplevel/class.mli @@ -0,0 +1,25 @@ + +(* $Id$ *) + +open Names +open Term +open Classops +open Declare + +val try_add_new_coercion : identifier -> strength -> unit +val try_add_new_coercion_subclass : identifier -> strength -> unit +val try_add_new_coercion_record: identifier -> strength -> section_path -> unit +val try_add_new_coercion_with_target : identifier -> strength -> + identifier -> identifier -> bool -> unit + +val try_add_new_class : identifier -> strength -> unit +val process_class : + section_path -> (cl_typ * cl_info_typ) -> (cl_typ * cl_info_typ) +val process_coercion : + section_path -> (coe_typ * coe_info_typ) * cl_typ * cl_typ -> + ((coe_typ * coe_info_typ) * cl_typ * cl_typ) * identifier * int + +val defined_in_sec : section_path -> section_path -> bool +val coercion_syntax : identifier -> int -> cl_typ -> unit +val fun_coercion_syntax_entry : identifier -> int -> unit +val coercion_syntax_entry : identifier -> int -> unit |