| Commit message (Expand) | Author | Age |
* | Fixes in generalize_eqs/dependent induction to allow the user to specify | msozeau | 2008-07-28 |
* | Fix wrong environment bug in test for setoid_rewrite or rewrite. | msozeau | 2008-07-28 |
* | Fix bug in term dnet preventing some unifications. Allow "higher-order" | msozeau | 2008-07-28 |
* | Even better test for choosing rewrite or setoid_rewrite. | msozeau | 2008-07-26 |
* | A better test for relations being setoids or not: do leibniz rewrite iff | msozeau | 2008-07-25 |
* | More compatibility fixes, revert the tauto fix that prevented | msozeau | 2008-07-25 |
* | Tauto breaking not only binary "conjunctions" seems like a bad idea | msozeau | 2008-07-24 |
* | A (safe) implementation of prolog's cut in the typeclasses eauto to avoid | msozeau | 2008-07-24 |
* | Suite commit 11236 | notin | 2008-07-24 |
* | Propagation de l'information "strict" (càd à toplevel ou en train de | herbelin | 2008-07-24 |
* | New tactics [conv] to test convertibility (actually, unification) of two | msozeau | 2008-07-22 |
* | A try at allowing matching on applications as a binary syntax node by default. | msozeau | 2008-07-22 |
* | Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d... | notin | 2008-07-18 |
* | Modification rapide du message d'erreur lorsqu'un _ ne peut être | herbelin | 2008-07-18 |
* | Uniformisation du format des messages d'erreur (commencent par une | herbelin | 2008-07-17 |
* | Quelques modifications autour du filtrage Ltac: | herbelin | 2008-07-16 |
* | Fix implicit arguments in sections bug and check for resolution of evars when | msozeau | 2008-07-07 |
* | Stop using the discrimination net in typeclasses/setoid rewrite, which was | msozeau | 2008-07-02 |
* | Enhanced discrimination nets implementation, which can now work with | msozeau | 2008-06-27 |
* | Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio... | notin | 2008-06-25 |
* | Rename obligations_tactic to obligation_tactic and fix bugs #1893. | msozeau | 2008-06-22 |
* | Correction petit bug sur révision 11159 (res_pf fait un effet de bord | herbelin | 2008-06-21 |
* | - Implantation de la suggestion 1873 sur discriminate. Au final, | herbelin | 2008-06-21 |
* | Little fixes: print unbound variable in error message (patch by Samuel | msozeau | 2008-06-19 |
* | incomplete bugfix for info | corbinea | 2008-06-19 |
* | Propagation des révisions 11144 et 11136 de la 8.2 vers le trunk | herbelin | 2008-06-18 |
* | Fix bug in implementation of splitting of class constraints. | msozeau | 2008-06-18 |
* | Compatibility fixes (Add Setoid bug and accidental introduction of a | msozeau | 2008-06-18 |
* | Fixes w.r.t. let binders in class contexts and Add Parametric | msozeau | 2008-06-17 |
* | Better typeclass error messages, always giving the full set of | msozeau | 2008-06-17 |
* | Add possibility to match on defined hypotheses, using brackets to | msozeau | 2008-06-16 |
* | Optionally (and by default) split typeclasses evars into connected | msozeau | 2008-06-11 |
* | - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs) | herbelin | 2008-06-10 |
* | - Correct handling of DependentMorphism error, using tclFAIL instead of | msozeau | 2008-06-10 |
* | Backtrack sur l'"optimisation" de admit (révision 11084). Comme le | herbelin | 2008-06-10 |
* | - Correction bug 1841 (identificateurs incorrects avec Subclass) | herbelin | 2008-06-10 |
* | - Correction de la version simplifiée (filtrage sur deux sig | herbelin | 2008-06-09 |
* | - Patch sur "intros until 0" | herbelin | 2008-06-08 |
* | - Extension de "generalize" en "generalize c as id at occs". | herbelin | 2008-06-08 |
* | Correct handling of the environment in build_signature, and throw | msozeau | 2008-06-07 |
* | Change setoid_rewrite's matching semantics to continue matching inside | msozeau | 2008-06-07 |
* | Enhancements to coqdoc, better globalization of sections and modules. | msozeau | 2008-06-06 |
* | Correctly catch UnresolvableConstraint exception which is now located. | msozeau | 2008-06-05 |
* | Fixes incorrect handling of existing existentials variables in | msozeau | 2008-06-03 |
* | Improvements on coqdoc by adding more information into .glob | msozeau | 2008-05-30 |
* | Improve the dependent induction tactic to automatically find the | msozeau | 2008-05-30 |
* | - Fix bug #1858, Hint Unfold calling the wrong locate function. | msozeau | 2008-05-23 |
* | Cleanup build_new, remove unneeded try-with and debug interaction of | msozeau | 2008-05-20 |
* | Fix globalization bug in class_tactics and refactorize instance | msozeau | 2008-05-19 |
* | Fix caml debug flags configuration, -g works with the native compiler only | msozeau | 2008-05-19 |