| Age | Commit message (Expand) | Author |
|---|
| 2008-06-19 | Little fixes: print unbound variable in error message (patch by Samuel | msozeau |
| 2008-06-18 | Improvements in subtac: | msozeau |
| 2008-06-18 | Compatibility fixes (Add Setoid bug and accidental introduction of a | msozeau |
| 2008-06-17 | Cleanup in subtac_cases, preparing to use improvements on return predicate | msozeau |
| 2008-06-03 | Fixes incorrect handling of existing existentials variables in | msozeau |
| 2008-05-30 | Improvements on coqdoc by adding more information into .glob | msozeau |
| 2008-05-23 | - Fix bug #1858, Hint Unfold calling the wrong locate function. | msozeau |
| 2008-05-15 | Various fixes: | msozeau |
| 2008-05-13 | - Fix bug related to indices of fixpoints. | msozeau |
| 2008-05-11 | - Cleanup parsing of binders, reducing to a single production for all | msozeau |
| 2008-05-06 | Postpone the search for the recursive argument index from the user given | msozeau |
| 2008-05-05 | Mise en place d'un algorithme d'inversion des contraintes de type lors | herbelin |
| 2008-04-26 | - Backtrack sur extension de syntaxe pour pose qui rentre en conflit avec | herbelin |
| 2008-04-25 | 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-23 | Prise en compte des coercions dans les clauses "with" même si le type | herbelin |
| 2008-04-17 | Little fixes in setoid_rewrite. | msozeau |
| 2008-04-15 | - Add "Global" modifier for instances inside sections with the usual | msozeau |
| 2008-04-13 | Bugs, nettoyage, et améliorations diverses | herbelin |
| 2008-04-12 | Add the ability to specify what to do with free variables in instance | msozeau |
| 2008-04-11 | Check that no evars remain in instance types earlier at Instance | msozeau |
| 2008-04-07 | Fix big de Bruijn bug in mutually recursive definitions. | msozeau |
| 2008-04-02 | Add the ability to specify the implicit status of section variables and | msozeau |
| 2008-04-01 | 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-03-28 | - Second pass on implementation of let pattern. Parse "let ' par [as x]? | msozeau |
| 2008-03-27 | Various fixes on typeclasses: | msozeau |
| 2008-03-23 | Fix a bug found by B. Grégoire when declaring morphisms in module | msozeau |
| 2008-03-19 | Do another pass on the typeclasses code. Correct globalization of class | msozeau |
| 2008-03-16 | Removed unneeded tactics from RelationClasses. Use | msozeau |
| 2008-03-16 | Minor fixes on setoid rewriting. Now uses definitions of [relation] and | msozeau |
| 2008-03-15 | Do a second pass on the treatment of user-given implicit arguments. Now | msozeau |
| 2008-03-10 | 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-09 | Fix a few bugs in Program: use user-given typing constraints for | msozeau |
| 2008-03-06 | Syntax changes in typeclasses, remove "?" for usual implicit arguments | msozeau |
| 2008-02-26 | Proper implicit arguments handling for assumptions | msozeau |
| 2008-02-22 | Merge with lmamane's private branch: | lmamane |
| 2008-02-10 | Backport Program Instance into Instance. Proper early error message if | msozeau |
| 2008-02-08 | 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-06 | New algorithm to resolve morphisms, after discussion with Nicolas | msozeau |
| 2008-01-31 | Fix obvious syntax error. Forgot to recompile before commiting... | msozeau |
| 2008-01-31 | Finish let| implementation and document it | msozeau |
| 2008-01-30 | 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-18 | Fix bug #1778, better typeclass error messages. Move Obligations Tactic to a ... | msozeau |
| 2008-01-17 | Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b... | msozeau |
| 2008-01-15 | Generalize instance declarations to any context, better name handling. Add ho... | msozeau |
