Versions initiales

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@136 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 67 insertions, 0 deletions

diff --git a/pretyping/classops.mli b/pretyping/classops.mli
new file mode 100644
index 0000000000..98716046f2
--- /dev/null
+++ b/pretyping/classops.mli
@@ -0,0 +1,67 @@
+
+(* $Id$ *)
+
+(*i*)
+open Pp
+open Names
+open Term
+open Evd
+open Environ
+open Libobject
+open Declare
+(*i*)
+
+type cl_typ = 
+  | CL_SORT 
+  | CL_FUN 
+  | CL_Var of identifier 
+  | CL_SP of section_path
+  | CL_IND of section_path * int
+
+type cl_info_typ = {
+  cL_STR : string;
+  cL_STRE : strength;
+  cL_PARAM : int }
+
+type cte_typ = 
+  | NAM_Var of identifier 
+  | NAM_SP of section_path 
+  | NAM_Construct of section_path * int * int
+
+type coe_typ = cte_typ
+
+
+type coe_info_typ = {
+  cOE_VALUE : unsafe_judgment;
+  cOE_STRE : strength;
+  cOE_ISID : bool;
+  cOE_PARAM : int }
+
+
+type inheritance_path = int list
+
+
+val cte_of_constr : constr -> cte_typ
+val class_info : cl_typ -> (int * cl_info_typ)
+val coercion_info : coe_typ -> (int * coe_info_typ)
+val constructor_at_head : constr -> cl_typ * int
+val class_of :  'c evar_map -> constr -> constr * int
+val class_args_of : constr -> constr list
+val inClass : (cl_typ * cl_info_typ) -> obj
+val outClass : obj -> (cl_typ * cl_info_typ)
+val inCoercion : (coe_typ * coe_info_typ) * cl_typ * cl_typ -> obj
+val outCoercion : obj -> (coe_typ * coe_info_typ) * cl_typ * cl_typ
+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
+val add_new_class : (cl_typ * string * strength * int) -> unit
+val add_new_coercion_in_graph : (coe_typ * coe_info_typ) * cl_typ * cl_typ -> unit
+val add_coercion_in_graph : int * int * int -> unit