| Age | Commit message (Expand) | Author |
|---|
| 2007-09-15 | * Adding compability with ocaml 3.10 + camlp5 (rework of | letouzey |
| 2007-09-14 | Correction du bug #1679 (congruence) et ajout test-suite | corbinea |
| 2007-09-06 | errors in recdef.ml4: | bertot |
| 2007-09-06 | this should fix a problem described in a message by Dufourd on July 30th, 2007 | bertot |
| 2007-08-31 | fin de la correction de Function | jforest |
| 2007-08-31 | correction bug d'efficacite dans Function | jforest |
| 2007-08-30 | Oubli dans commit 10102... | herbelin |
| 2007-08-29 | - Débogueur: positionnement de set_detype_anonymous pour ne pas | herbelin |
| 2007-08-27 | Oubli dans la révision 10098 (nettoyage body_of_type) | herbelin |
| 2007-08-27 | Suppression des type_app et body_of_type qui alourdissent inutilement le code | herbelin |
| 2007-08-26 | Fix bug on wellfounded defs with constant parameters and dependencies on the ... | msozeau |
| 2007-08-26 | Fix de Bruijn bug in wf definitions. | msozeau |
| 2007-08-26 | Fix evars bug in mutual fixpoints with implicit types and bug in inequalities... | msozeau |
| 2007-08-16 | Correction du bug #1680: ajout d'un champ avoid_ids dans interp_sign; | notin |
| 2007-08-08 | Fix dependency bugs due to Program modules renamings. | msozeau |
| 2007-08-07 | Move Program tactics into a proper theories/ directory as they are general pu... | msozeau |
| 2007-07-24 | fixed bug 1448 and 1674 | barras |
| 2007-07-24 | fixed bug 1675: computing carrier from the relation type was not right | barras |
| 2007-07-24 | Declarative language: fixed the generation of fixpoints for induction proofs. | corbinea |
| 2007-07-19 | Documentation of Program and its tactics, fix enormous interaction bug due to... | msozeau |
| 2007-07-18 | A generic preprocessing tactic zify for (r)omega | letouzey |
| 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 |
