| Age | Commit message (Expand) | Author |
| 2007-07-16 | Generalized CAMLP4USE for pp dependencies | corbinea |
| 2007-07-13 | some more useless constant in const_omega | letouzey |
| 2007-07-13 | Beginning of a reorganisation of the ml part for romega: | letouzey |
| 2007-07-13 | removing a warning at compilation time | jforest |
| 2007-07-12 | Deletion of contrib/extraction/test | letouzey |
| 2007-07-12 | normalisation (by closure) was not performed under fixpoints | barras |
| 2007-07-12 | port de r9968: bug avec les ring calculatoires | barras |
| 2007-07-12 | An optimization to simplify generated obligations removing unnecessary let-in's. | msozeau |
| 2007-07-12 | Fix bug when adding progs with no obligations | msozeau |
| 2007-07-12 | Remove dead modules in Subtac. | msozeau |
| 2007-07-12 | Cleanup, use Util list functions when possible | msozeau |
| 2007-07-11 | Slight cleanup of refl_omega.ml : in particular it uses now list | letouzey |
| 2007-07-10 | Big reorganization of romega/ReflOmegaCore.v: towards a modular | letouzey |
| 2007-07-09 | Improvements / Bug fixes for ROmega | letouzey |
| 2007-07-06 | minor bug correction (continuing r 9943) | jforest |
| 2007-07-06 | Adding a syntax for "n-ary" rewrite: | letouzey |
| 2007-07-06 | sequel to commit 9952: forgot to adapt xlate to the new n-ary rename | letouzey |
| 2007-07-06 | extension of the rename tactic: the following is now allowed: | letouzey |
| 2007-07-06 | New intro pattern "@A", which generates a fresh name based on A. | glondu |
| 2007-07-05 | Minor bug correction in Function. Non terminating Function e.g. | jforest |
| 2007-07-02 | Better handling of aliases, add command to solve a particular obligation. | msozeau |
| 2007-06-26 | killing some more non-exhaustive patterns | letouzey |
| 2007-06-21 | Correction de plusieurs bugs de l'export XML (utilisation d'un type de | herbelin |
| 2007-06-14 | Add Solve All Obligations command, fix bug in inequality generation introduce... | msozeau |
| 2007-06-09 | Various Program fixes, multiple pattern matches, aliases. Fix bug in coercion... | msozeau |
| 2007-06-07 | Extension of NArith: Nminus, Nmin, etc | letouzey |
| 2007-06-07 | Unification des types + clause filtrage manquante + uniformisation locale | herbelin |
| 2007-05-25 | Modification of VernacScheme to handle a new scheme: Equality (equality in | vsiles |
| 2007-05-24 | fixed (PR#1483) | corbinea |
| 2007-05-22 | Nouvelle stratégie d'unification des types des with-bindings dans | herbelin |
| 2007-05-20 | - Propagation des evars non résolues vers les with_bindings; permet par exemple | herbelin |
| 2007-05-17 | correction de bug dans Function et augmentation de la classe des fonctions su... | jforest |
| 2007-05-11 | Processor integers + Print assumption (see coqdev mailing list for the | aspiwack |
| 2007-05-06 | Nouveaux changements autour des implicites (notamment suite à | herbelin |
| 2007-04-29 | Orthographe en passant | herbelin |
| 2007-04-29 | Ajout possibilité d'options à trois mots. | herbelin |
| 2007-04-28 | Ajout de la possibilité de faire référence dans certains cas à un nom | herbelin |
| 2007-04-28 | Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in. | herbelin |
| 2007-04-25 | New keyword "Inline" for Parameters and Axioms for automatic | soubiran |
| 2007-04-17 | Correct implementation of undo in obligations handling code, correct some bug... | msozeau |
| 2007-04-16 | Export de simplest_eapply, utilisé dans la contrib interface | notin |
| 2007-04-05 | Mise en place d'une nouvelle strategie plus efficace pour les preuves de Func... | jforest |
| 2007-04-02 | Extension to the general sequence operator (tactical). Now in addition to ... | emakarov |
| 2007-03-28 | Support for implicit formal argument types in Program ; parse types in type s... | msozeau |
| 2007-03-26 | Make multiple patterns work again with Program while simplifying the code. | msozeau |
| 2007-03-20 | Some tactic fixes in Subtac, fix obvious bug in admit_obligations but still a... | msozeau |
| 2007-03-20 | traces Ergo | filliatr |
| 2007-03-19 | Forgot to update to new cast | msozeau |
| 2007-03-19 | Add a parameter to QuestionMark evar kind to say it can be turned into an obl... | msozeau |
| 2007-03-16 | r11153@tannat: jforest | 2007-03-16 10:25:55 +0100 | jforest |