diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-01-07 22:20:58 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-01-07 22:20:58 +0000 |
| commit | 805b6b2776866acd2cf94d8ce72eabd7cebbefe1 (patch) | |
| tree | 6ba21cb7811f8e2affb99c9027e7791f85b599a3 /pretyping/classops.mli | |
| parent | 4fb95ddde5870ab484f9d154bd406f344e6f88d5 (diff) | |
Déplacement non-affichage des coercions dans termast
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@264 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/classops.mli')
| -rw-r--r-- | pretyping/classops.mli | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/pretyping/classops.mli b/pretyping/classops.mli index fe7fb437d..5aa8b7aaf 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -9,6 +9,7 @@ open Evd open Environ open Libobject open Declare +open Rawterm (*i*) type cl_typ = @@ -25,8 +26,9 @@ type cl_info_typ = { type cte_typ = | NAM_Var of identifier - | NAM_SP of section_path - | NAM_Construct of constructor_path + | NAM_Constant of section_path + | NAM_Inductive of inductive_path + | NAM_Constructor of constructor_path type coe_typ = cte_typ @@ -50,6 +52,7 @@ 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 coercion_params : reference -> int (* raise Not_found if not a coercion *) 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 |