From 1cd1801ee86d6be178f5bce700633aee2416d236 Mon Sep 17 00:00:00 2001 From: msozeau Date: Wed, 28 Oct 2009 22:51:46 +0000 Subject: Integrate a few improvements on typeclasses and Program from the equations branch and remove equations stuff which moves to a separate plugin. Classes: - Ability to define classes post-hoc from constants or inductive types. - Correctly rebuild the hint database associated to local hypotheses when they are changed by a [Hint Extern] in typeclass resolution. Tactics and proofs: - Change [revert] so that it keeps let-ins (but not [generalize]). - Various improvements to the [generalize_eqs] tactic to make it more robust and produce the smallest proof terms possible. Move [specialize_hypothesis] in tactics.ml as it goes hand in hand with [generalize_eqs]. - A few new general purpose tactics in Program.Tactics like [revert_until] - Make transitive closure well-foundedness proofs transparent. - More uniform testing for metas/evars in pretyping/unification.ml (might introduce a few changes in the contribs). Program: - Better sorting of dependencies in obligations. - Ability to start a Program definition from just a type and no obligations, automatically adding an obligation for this type. - In compilation of Program's well-founded definitions, make the functional a separate definition for easier reasoning. - Add a hint database for every Program populated by [Hint Unfold]s for every defined obligation constant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12440 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/typeclasses.mli | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) (limited to 'pretyping/typeclasses.mli') diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index c9ee9adf0..19ec47cf4 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -49,7 +49,11 @@ val all_instances : unit -> instance list val add_class : typeclass -> unit -val new_instance : typeclass -> int option -> bool -> constant -> instance +val add_constant_class : constant -> unit + +val add_inductive_class : inductive -> unit + +val new_instance : typeclass -> int option -> bool -> global_reference -> instance val add_instance : instance -> unit val class_info : global_reference -> typeclass (* raises a UserError if not a class *) @@ -60,8 +64,8 @@ val dest_class_app : env -> constr -> typeclass * constr list (* Just return None if not a class *) val class_of_constr : constr -> typeclass option - -val instance_impl : instance -> constant + +val instance_impl : instance -> global_reference val is_class : global_reference -> bool val is_instance : global_reference -> bool @@ -86,8 +90,11 @@ val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool -> env -> evar_defs -> evar_defs val resolve_one_typeclass : env -> evar_map -> types -> open_constr -val register_add_instance_hint : (constant -> int option -> unit) -> unit -val add_instance_hint : constant -> int option -> unit +val register_set_typeclass_transparency : (evaluable_global_reference -> bool -> unit) -> unit +val set_typeclass_transparency : evaluable_global_reference -> bool -> unit + +val register_add_instance_hint : (global_reference -> int option -> unit) -> unit +val add_instance_hint : global_reference -> int option -> unit val solve_instanciations_problem : (env -> evar_defs -> bool -> bool -> bool -> evar_defs) ref val solve_instanciation_problem : (env -> evar_map -> types -> open_constr) ref -- cgit v1.2.3