aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/typeclasses.mli
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-04-02 15:47:07 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-04-02 15:47:07 +0000
commit46cad49197abd858ef430c150e32702c01b2f205 (patch)
tree714d2ef2858e862f9233955260ed1d47e9963404 /pretyping/typeclasses.mli
parentbf9d5245c59e297d93ee759f54b40ec67db5ff93 (diff)
Add the ability to specify the implicit status of section variables and
whether or not to keep them regardless of the actual dependencies (in order to implement the proper discharge behavior for type classes). This means adding an argument to rebuild_function in libobject, giving this information on variables after a section's constants have been discharged (discharge_function is too early). Surface syntax for Variable not added yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10741 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/typeclasses.mli')
-rw-r--r--pretyping/typeclasses.mli7
1 files changed, 2 insertions, 5 deletions
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 2646c09dd..c091842f0 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -52,8 +52,8 @@ val typeclasses : unit -> typeclass list
val add_class : typeclass -> unit
val add_instance : instance -> unit
-val register_add_instance_hint : (reference -> int option -> unit) -> unit
-val add_instance_hint : reference -> int option -> unit
+val register_add_instance_hint : (constant -> int option -> unit) -> unit
+val add_instance_hint : constant -> int option -> unit
val class_info : global_reference -> typeclass (* raises a UserError if not a class *)
val is_class : global_reference -> bool
@@ -89,9 +89,6 @@ val nf_substitution : evar_map -> substitution -> substitution
val is_implicit_arg : hole_kind -> bool
-val qualid_of_con : Names.constant -> Libnames.reference
-
-
(* debug *)
(* val subst : *)