| Commit message (Expand) | Author | Age |
|---|
| * | Improvements on coqdoc by adding more information into .glob |  msozeau | 2008-05-30 |
| * | - Fix bug #1858, Hint Unfold calling the wrong locate function. | msozeau | 2008-05-23 |
| * | Various fixes: | msozeau | 2008-05-15 |
| * | - Fix bug related to indices of fixpoints. | msozeau | 2008-05-13 |
| * | - Cleanup parsing of binders, reducing to a single production for all | msozeau | 2008-05-11 |
| * | Postpone the search for the recursive argument index from the user given | msozeau | 2008-05-06 |
| * | Mise en place d'un algorithme d'inversion des contraintes de type lors |  herbelin | 2008-05-05 |
| * | - Backtrack sur extension de syntaxe pour pose qui rentre en conflit avec | herbelin | 2008-04-26 |
| * | Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve | herbelin | 2008-04-25 |
| * | - Fix bug in eterm which was not taking filtered contexts in evars into | msozeau | 2008-04-25 |
| * | Prise en compte des coercions dans les clauses "with" même si le type | herbelin | 2008-04-23 |
| * | Little fixes in setoid_rewrite. | msozeau | 2008-04-17 |
| * | - Add "Global" modifier for instances inside sections with the usual | msozeau | 2008-04-15 |
| * | Bugs, nettoyage, et améliorations diverses | herbelin | 2008-04-13 |
| * | Add the ability to specify what to do with free variables in instance | msozeau | 2008-04-12 |
| * | Check that no evars remain in instance types earlier at Instance | msozeau | 2008-04-11 |
| * | Fix big de Bruijn bug in mutually recursive definitions. | msozeau | 2008-04-07 |
| * | Add the ability to specify the implicit status of section variables and | msozeau | 2008-04-02 |
| * | Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient | herbelin | 2008-04-01 |
| * | Add option to set the opacity of obligations to transparent, to be able | msozeau | 2008-04-01 |
| * | - Second pass on implementation of let pattern. Parse "let ' par [as x]? | msozeau | 2008-03-28 |
| * | Various fixes on typeclasses: | msozeau | 2008-03-27 |
| * | Fix a bug found by B. Grégoire when declaring morphisms in module | msozeau | 2008-03-23 |
| * | Do another pass on the typeclasses code. Correct globalization of class | msozeau | 2008-03-19 |
| * | Removed unneeded tactics from RelationClasses. Use | msozeau | 2008-03-16 |
| * | Minor fixes on setoid rewriting. Now uses definitions of [relation] and | msozeau | 2008-03-16 |
| * | Do a second pass on the treatment of user-given implicit arguments. Now | msozeau | 2008-03-15 |
| * | Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145) | herbelin | 2008-03-10 |
| * | Fix compilation problem and finish little cleanup. | msozeau | 2008-03-10 |
| * | Fix a few bugs in Program: use user-given typing constraints for | msozeau | 2008-03-09 |
| * | Syntax changes in typeclasses, remove "?" for usual implicit arguments | msozeau | 2008-03-06 |
| * | Proper implicit arguments handling for assumptions | msozeau | 2008-02-26 |
| * | Merge with lmamane's private branch: |  lmamane | 2008-02-22 |
| * | Backport Program Instance into Instance. Proper early error message if | msozeau | 2008-02-10 |
| * | Change implementation of resolution for typeclasses to use a customized | msozeau | 2008-02-08 |
| * | New "Preterm [ of id ] " command to show the preterm before giving it to | msozeau | 2008-02-08 |
| * | Backport code from command.ml to subtac_command.ml for definining | msozeau | 2008-02-08 |
| * | New algorithm to resolve morphisms, after discussion with Nicolas | msozeau | 2008-02-06 |
| * | Fix obvious syntax error. Forgot to recompile before commiting... | msozeau | 2008-01-31 |
| * | Finish let| implementation and document it | msozeau | 2008-01-31 |
| * | Work on dependent induction tactic and friends, finish the test-suite example | msozeau | 2008-01-30 |
| * | Use new redefinition support for the default obligations tactic | msozeau | 2008-01-30 |
| * | Fix bug #1778, better typeclass error messages. Move Obligations Tactic to a ... | msozeau | 2008-01-18 |
| * | Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b... | msozeau | 2008-01-17 |
| * | Generalize instance declarations to any context, better name handling. Add ho... | msozeau | 2008-01-15 |
| * | Cleaner quantifiers for type classes, breaks clrewrite for the moment but imp... | msozeau | 2008-01-07 |
| * | Add partial setoids in theories/Classes, add SetoidDec class for setoids with... | msozeau | 2008-01-04 |
| * | Fix name capture bug and call the right pretyper in subtac. | msozeau | 2007-12-31 |
| * | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau | 2007-12-31 |
| * | Plus de combinateurs sont passés de Util à Option. Le module Options |  aspiwack | 2007-12-06 |
msozeau
herbelin
lmamane
aspiwack