Merge subinstances branch by me and Tom Prince.

This adds two experimental features to the typeclass implementation:
- Path cuts: a way to specify through regular expressions on instance names
search pathes that should be avoided (e.g. [proper_flip proper_flip]).
Regular expression matching is implemented through naïve derivatives.
- Forward hints for subclasses: e.g. [Equivalence -> Reflexive] is no
longer applied backwards, but introducing a specific [Equivalence] in the
environment register a [Reflexive] hint as well. Currently not
backwards-compatible, the next patch will allow to specify direction
of subclasses hints.

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

1 files changed, 15 insertions, 4 deletions

diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index e4db68fbc..a00d23a9b 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -34,8 +34,9 @@ type typeclass = {
 
   (** The methods implementations of the typeclass as projections. 
       Some may be undefinable due to sorting restrictions or simply undefined if 
-      no name is provided. The boolean indicates subclasses. *)
-  cl_projs : (name * bool * constant option) list;
+      no name is provided. The [int option option] indicates subclasses whose hint has
+      the given priority. *)
+  cl_projs : (name * int option option * constant option) list;
 }
 
 type instance
@@ -93,10 +94,20 @@ val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> u
 val register_classes_transparent_state : (unit -> transparent_state) -> unit
 val classes_transparent_state : unit -> transparent_state
 
-val register_add_instance_hint : (global_reference -> bool (* local? *) -> int option -> unit) -> unit
+val register_add_instance_hint : (constr -> bool (* local? *) -> int option -> unit) -> unit
 val register_remove_instance_hint : (global_reference -> unit) -> unit
-val add_instance_hint : global_reference -> bool -> int option -> unit
+val add_instance_hint : constr -> bool -> int option -> unit
 val remove_instance_hint : global_reference -> unit
 
 val solve_instanciations_problem : (env -> evar_map -> bool -> bool -> bool -> evar_map) ref
 val solve_instanciation_problem : (env -> evar_map -> types -> open_constr) ref
+
+val declare_instance : int option -> bool -> global_reference -> unit
+
+
+(** Build the subinstances hints for a given typeclass object.
+    check tells if we should check for existence of the 
+    subinstances and add only the missing ones. *)
+
+val build_subclasses : check:bool -> env -> evar_map -> global_reference -> int option (* priority *) ->
+  (int option * constr) list