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 --- theories/Wellfounded/Transitive_Closure.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'theories/Wellfounded') diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v index bce32af48..c999b58ee 100644 --- a/theories/Wellfounded/Transitive_Closure.v +++ b/theories/Wellfounded/Transitive_Closure.v @@ -29,7 +29,7 @@ Section Wf_Transitive_Closure. intros y H2. induction H2; auto with sets. apply Acc_inv with y; auto with sets. - Qed. + Defined. Hint Resolve Acc_clos_trans. @@ -42,6 +42,6 @@ Section Wf_Transitive_Closure. Theorem wf_clos_trans : well_founded R -> well_founded trans_clos. Proof. unfold well_founded in |- *; auto with sets. - Qed. + Defined. End Wf_Transitive_Closure. -- cgit v1.2.3