| Commit message (Expand) | Author | Age |
|---|
| * | Check [Equations] patterns are for the right function. |  msozeau | 2008-09-07 |
| * | More debugging of [Equations], now able to discharge even the heavily | msozeau | 2008-09-07 |
| * | Better handling of the opacity of proof obligations, add the possibility of | msozeau | 2008-09-07 |
| * | Better handling of recursive Equations definitions... still not perfect. | msozeau | 2008-09-03 |
| * | Correct handling of implicit arguments in [Equations] definitions, | msozeau | 2008-09-03 |
| * | Add support for recursive definitions to [Equations], deciding if a | msozeau | 2008-09-02 |
| * | Initial implementation of a new command to define (dependent) functions by | msozeau | 2008-09-02 |
| * | - Remove some dead code in subtac | msozeau | 2008-09-02 |
| * | Propagating commit 11343 from branch v8.2 to trunk (wish 1934 about |  herbelin | 2008-09-02 |
| * | Give back progress information after feeding the Program Instance to the | msozeau | 2008-08-26 |
| * | Various fixes w.r.t typeclasses and subtac: resolve tcs properly inside | msozeau | 2008-08-21 |
| * | Évolutions diverses et variées. | herbelin | 2008-08-04 |
| * | Fix bug #1913, checking for unresolved evars which aren't obligations. | msozeau | 2008-07-24 |
| * | Suite commit 11236 |  notin | 2008-07-24 |
| * | Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d... | notin | 2008-07-18 |
| * | Correct a bug in the coercion code where we did not go under constants | msozeau | 2008-07-02 |
| * | Various bug fixes in type classes and subtac: | msozeau | 2008-07-01 |
| * | 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 |
| * | Code cleanup in typeclasses, remove dead and duplicated code. | msozeau | 2008-06-21 |
| * | Various improvements in handling of evars in general and typing | msozeau | 2008-06-21 |
| * | Little fixes: print unbound variable in error message (patch by Samuel | msozeau | 2008-06-19 |
| * | Improvements in subtac: | msozeau | 2008-06-18 |
| * | Compatibility fixes (Add Setoid bug and accidental introduction of a | msozeau | 2008-06-18 |
| * | Cleanup in subtac_cases, preparing to use improvements on return predicate | msozeau | 2008-06-17 |
| * | 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 |
| * | - 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 |
msozeau
herbelin
notin