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/recordops.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/recordops.mli')
-rwxr-xr-x | pretyping/recordops.mli | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 4d28ee55b..5d3180ff7 100755 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -22,12 +22,12 @@ open Library constructor (the name of which defaults to Build_S) *) type struc_typ = { - s_CONST : constructor; + s_CONST : constructor; s_EXPECTEDPARAM : int; s_PROJKIND : (name * bool) list; s_PROJ : constant option list } -val declare_structure : +val declare_structure : inductive * constructor * (name * bool) list * constant option list -> unit (* [lookup_projections isp] returns the projections associated to the @@ -46,8 +46,8 @@ val find_projection : global_reference -> struc_typ val declare_method : global_reference -> Evd.evar -> Evd.evar_map -> unit (* and here is how to search for methods matched by a given term: *) -val methods_matching : constr -> - ((global_reference*Evd.evar*Evd.evar_map) * +val methods_matching : constr -> + ((global_reference*Evd.evar*Evd.evar_map) * (constr*existential_key)*Termops.subst) list (*s A canonical structure declares "canonical" conversion hints between *) @@ -56,7 +56,7 @@ val methods_matching : constr -> type cs_pattern = Const_cs of global_reference - | Prod_cs + | Prod_cs | Sort_cs of sorts_family | Default_cs @@ -69,10 +69,10 @@ type obj_typ = { o_TCOMPS : constr list } (* ordered *) val cs_pattern_of_constr : constr -> cs_pattern * int * constr list - + val lookup_canonical_conversion : (global_reference * cs_pattern) -> obj_typ val declare_canonical_structure : global_reference -> unit val is_open_canonical_projection : Evd.evar_map -> (constr * constr list) -> bool -val canonical_projections : unit -> +val canonical_projections : unit -> ((global_reference * cs_pattern) * obj_typ) list |