diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-17 15:58:14 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-17 15:58:14 +0000 |
| commit | 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch) | |
| tree | 961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /pretyping/classops.mli | |
| parent | 6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff) | |
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/classops.mli')
| -rw-r--r-- | pretyping/classops.mli | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/pretyping/classops.mli b/pretyping/classops.mli index a5f139ab1..63d5b0a4e 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -19,9 +19,9 @@ open Mod_subst (*i*) (*s This is the type of class kinds *) -type cl_typ = - | CL_SORT - | CL_FUN +type cl_typ = + | CL_SORT + | CL_FUN | CL_SECVAR of variable | CL_CONST of constant | CL_IND of inductive @@ -36,7 +36,7 @@ type cl_info_typ = { type coe_typ = Libnames.global_reference (* This is the type of infos for declared coercions *) -type coe_info_typ +type coe_info_typ (* [cl_index] is the type of class keys *) type cl_index @@ -65,7 +65,7 @@ val inductive_class_of : inductive -> cl_index val class_args_of : env -> evar_map -> types -> constr list (*s [declare_coercion] adds a coercion in the graph of coercion paths *) -val declare_coercion : +val declare_coercion : coe_typ -> locality -> isid:bool -> src:cl_typ -> target:cl_typ -> params:int -> unit @@ -77,18 +77,18 @@ val coercion_value : coe_index -> (unsafe_judgment * bool) (*s Lookup functions for coercion paths *) val lookup_path_between_class : cl_index * cl_index -> inheritance_path -val lookup_path_between : env -> evar_map -> types * types -> +val lookup_path_between : env -> evar_map -> types * types -> types * types * inheritance_path val lookup_path_to_fun_from : env -> evar_map -> types -> types * inheritance_path -val lookup_path_to_sort_from : env -> evar_map -> types -> +val lookup_path_to_sort_from : env -> evar_map -> types -> types * inheritance_path -val lookup_pattern_path_between : +val lookup_pattern_path_between : inductive * inductive -> (constructor * int) list (*i Crade *) open Pp -val install_path_printer : +val install_path_printer : ((cl_index * cl_index) * inheritance_path -> std_ppcmds) -> unit (*i*) |