| Age | Commit message (Expand) | Author |
|---|
| 2007-07-13 | Beginning of a reorganisation of the ml part for romega: | letouzey |
| 2007-07-13 | A emacs-specific comment to use makefile-mode on Makefile.* | letouzey |
| 2007-07-13 | Added Qpower_plus' and Zpower_Qpower | roconnor |
| 2007-07-13 | Small cleanup | letouzey |
| 2007-07-13 | Répertoire Numbers poursuit l'objectif entamé en syntaxe V7 dans le | herbelin |
| 2007-07-13 | Deletion of some firstorder calls in FSetAVL: | letouzey |
| 2007-07-13 | New bootstrapping, improved, Makefile system | corbinea |
| 2007-07-13 | removing a warning at compilation time | jforest |
| 2007-07-12 | Proof for sub | thery |
| 2007-07-12 | (Port of r9984) Easier debugging: | glondu |
| 2007-07-12 | Update (test-suite was not successful). | glondu |
| 2007-07-12 | Deletion of an obsolete file (euclidian division done in old syntax with real... | letouzey |
| 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 | Forgot to commit new Makefile | msozeau |
| 2007-07-12 | Remove dead modules in Subtac. | msozeau |
| 2007-07-12 | Cleanup, use Util list functions when possible | msozeau |
| 2007-07-12 | Proof for succ, add, pred | thery |
| 2007-07-11 | dead code | letouzey |
| 2007-07-11 | Slight cleanup of refl_omega.ml : in particular it uses now list | letouzey |
| 2007-07-11 | Added ForAll_Str_nth_tl | roconnor |
| 2007-07-10 | Big reorganization of romega/ReflOmegaCore.v: towards a modular | letouzey |
| 2007-07-09 | Petites corrections sur le Makefile | notin |
| 2007-07-09 | More natural notation for intro pattern: @a -> ?a | glondu |
| 2007-07-09 | Improvements / Bug fixes for ROmega | letouzey |
| 2007-07-07 | If a fixpoint is not written with an explicit { struct ... }, then | letouzey |
| 2007-07-06 | a few works about my commits since February | letouzey |
| 2007-07-06 | minor bug correction (continuing r 9943) | jforest |
| 2007-07-06 | Update of theories/Numbers directory. | emakarov |
| 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 | Documentation for commit 9774. | glondu |
| 2007-07-06 | New intro pattern "@A", which generates a fresh name based on A. | glondu |
| 2007-07-06 | Documentation related to commit 9948: intropattern {A,B,C} for (A,(B,C)) | letouzey |
| 2007-07-06 | Suggestion of additional syntax for intro patterns: | letouzey |
| 2007-07-05 | Update on numbers. | emakarov |
| 2007-07-05 | Added Qpower_mult theorem. | roconnor |
| 2007-07-05 | documentation of f_equal and revert and case_eq (and s/lri.fr/pps.jussieu.fr/... | letouzey |
| 2007-07-05 | Minor bug correction in Function. Non terminating Function e.g. | jforest |
| 2007-07-03 | Compatibilité des noms longs de Bool déplacés dans Datatypes | herbelin |
| 2007-07-02 | Correction (partielle) du bug #1587 | notin |
| 2007-07-02 | Missing include path of ocaml .h when generating deps | msozeau |
| 2007-07-02 | Better handling of aliases, add command to solve a particular obligation. | msozeau |
| 2007-07-02 | Fix bug in subst_cases_pattern when aliasing recursive notations. | msozeau |
| 2007-07-02 | Factorisation des paramètres dans l'affichage des inductifs | herbelin |
| 2007-06-30 | Correction bug sur factorisation affichage paramètres (cf r9918) | herbelin |
