| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2007-06-30 | Factorisation des types dans l'affichage des paramètres des (Co)Inductif/Record | herbelin |
| 2007-06-30 | - Ajout de la possibilité d'utiliser la notation Record pour les | herbelin |
| 2007-06-29 | Added the directory theories/Numbers where axiomatizations and implementation... | emakarov |
| 2007-06-27 | - Extensions of FMap(Weak)Facts: | letouzey |
| 2007-06-27 | eqlistA is now equivlistA | letouzey |
| 2007-06-26 | killing some more non-exhaustive patterns | letouzey |
| 2007-06-26 | kill an ugly warning about a non-exhaustive pattern | letouzey |
| 2007-06-26 | Oups: thanks to ./configure -reals no, I was not building the whole dependenc... | letouzey |
| 2007-06-26 | Added zwqipWith. | roconnor |
| 2007-06-26 | additional properties for FMap (and slight rework of SetoidList and FSetPrope... | letouzey |
| 2007-06-25 | Updated Qpow_tac to work on a a more realistic set of exponent values. | roconnor |
| 2007-06-22 | Ajout exist & cie à la table des hints par symétrie avec ex_intro & | herbelin |
| 2007-06-21 | Correction de 2 bugs mineurs: 1 ligne de debug oubliée dans coqdoc, | notin |
| 2007-06-21 | Simplification de la construction du .depend: | notin |
| 2007-06-21 | Correction de plusieurs bugs de l'export XML (utilisation d'un type de | herbelin |
| 2007-06-21 | Adding: Field instance for Q. | roconnor |
| 2007-06-20 | ajout de head0 et tail0 en natif | bgregoir |
| 2007-06-19 | safe_shift correct recursion | thery |
| 2007-06-19 | safe_shift recursion | thery |
| 2007-06-19 | safe_shift recursion | thery |
| 2007-06-19 | typo faq | herbelin |
| 2007-06-19 | Adding function is_even, safe_shiftl, safe_shiftr | thery |
