| Commit message (Expand) | Author | Age |
|---|
| * | 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-12 |
| * | 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-11 |
| * | Big reorganization of romega/ReflOmegaCore.v: towards a modular | letouzey | 2007-07-10 |
| * | 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-09 |
| * | If a fixpoint is not written with an explicit { struct ... }, then | letouzey | 2007-07-07 |
| * | 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-06 |
| * | 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-05 |
| * | Compatibilité des noms longs de Bool déplacés dans Datatypes |  herbelin | 2007-07-03 |
| * | 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-07-02 |
| * | 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-30 |
| * | Added the directory theories/Numbers where axiomatizations and implementation... | emakarov | 2007-06-29 |
| * | - Extensions of FMap(Weak)Facts: | letouzey | 2007-06-27 |
| * | eqlistA is now equivlistA | letouzey | 2007-06-27 |
| * | 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-26 |
| * | Updated Qpow_tac to work on a a more realistic set of exponent values. | roconnor | 2007-06-25 |
letouzey
barras
msozeau
thery
roconnor
notin
glondu
jforest
emakarov
herbelin