diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-20 08:40:03 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-20 08:40:03 +0000 |
| commit | 2c82358cdfdcebfa9a39a6259b67f0a611f7cf22 (patch) | |
| tree | 3ac81998337e0cc22cc401bff91b5e8d183fafa3 /toplevel/class.mli | |
| parent | 31c8f44cfd250b0b4d77a25bf4339f4fab2f55c0 (diff) | |
Mieux à sa place dans toplevel
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@858 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/class.mli')
| -rw-r--r-- | toplevel/class.mli | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/toplevel/class.mli b/toplevel/class.mli new file mode 100644 index 000000000..e88b3ccf0 --- /dev/null +++ b/toplevel/class.mli @@ -0,0 +1,24 @@ + +(* $Id$ *) + +(*i*) +open Names +open Term +open Classops +open Declare +(*i*) + +(* Classes and coercions. *) + +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 -> identifier -> 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 : + dir_path -> (cl_typ * cl_info_typ) -> (cl_typ * cl_info_typ) +val process_coercion : + dir_path -> (coe_typ * coe_info_typ) * cl_typ * cl_typ -> + ((coe_typ * coe_info_typ) * cl_typ * cl_typ) * identifier * int |