| Age | Commit message (Expand) | Author |
|---|
| 2009-09-11 | Generalized the possibility to refer to a global name by a notation | herbelin |
| 2009-09-11 | Add doc of [Context] vernacular. | msozeau |
| 2009-09-11 | Added the following lemmas to homogenize Reals a bit: | gmelquio |
| 2009-09-11 | Removed Gappa from the external provers supported by the dp plugin. Tactic ga... | gmelquio |
| 2009-09-11 | - Resolve type class constraints before trying to find unresolved | msozeau |
| 2009-09-10 | Fixes for toc depth handling and handling of substitles from Chris Casinghino. | msozeau |
| 2009-09-10 | Misc fixes: | msozeau |
| 2009-09-10 | Added syntax "exists bindings, ..., bindings" for iterated "exists". | herbelin |
| 2009-09-09 | Allow setoid rewrite to rewrite in pattern-matching scrutinees or | msozeau |
| 2009-09-09 | Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvements | letouzey |
| 2009-09-09 | Stop trying to search if the relation is declared as a [RewriteRelation] | msozeau |
| 2009-09-08 | Update coqdoc documentation, CHANGES and add a fix for the proofbox (patch | msozeau |
| 2009-09-08 | Fix the bug-ridden code used to choose leibniz or generalized | msozeau |
| 2009-09-07 | ajout CVC3; ajout traduction des reels | marche |
| 2009-09-04 | Incorporate coqdoc changes by the UPenn team (B.Pierce, C. Casinghino, | msozeau |
| 2009-09-03 | Add --plain-comments patch by F. Garillot, which also adds | msozeau |
| 2009-09-03 | Support globality flag properly for "Add Morphism foo : foo_mor" syntax. | msozeau |
| 2009-09-03 | Remove unnecessary redefinitions of [Fix_sub] and [Fix_F_sub], as | msozeau |
| 2009-09-02 | Postpone checking of Local/Global to allow grammar extensions to use it | msozeau |
| 2009-09-02 | Stop unnecessary use of lazy values for constraints, simplifying | msozeau |
| 2009-09-02 | Hack to correctly get ill-formed rec body exceptions even | msozeau |
| 2009-08-31 | Fix notation for ~x in theories/Unicode/Utf8.v | glondu |
| 2009-08-29 | Fix minor spelling error | glondu |
| 2009-08-28 | update for why 2.19 | marche |
| 2009-08-27 | Correction bug 2140. | soubiran |
| 2009-08-25 | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12294 85f007b7-540e-0... | fbesson |
| 2009-08-25 | Delegate _all_ doc targets to stage2 | lmamane |
| 2009-08-25 | install-doc* are PHONY | lmamane |
| 2009-08-24 | New tactic to rewrite decidability lemmas when one knows which side | herbelin |
| 2009-08-23 | A new kind of automatically generated scheme "congr" for equality types | herbelin |
| 2009-08-23 | Fix a small oversight in checker commit 12288. | herbelin |
| 2009-08-22 | Transfers to checker ("let"s in inductive arities + Coq root read-only). | herbelin |
| 2009-08-20 | new csdp cache + improved error message | fbesson |
| 2009-08-20 | new csdp cache + improved error message | fbesson |
| 2009-08-19 | adds a property on map | bertot |
| 2009-08-19 | adds lemmas on interactions between existsb, forallb, and app | bertot |
| 2009-08-15 | + csdp.cache | fbesson |
| 2009-08-14 | Mise à jour du document de révision de la stdlib et déplacement de la | herbelin |
| 2009-08-14 | +Fix interface. | aspiwack |
| 2009-08-14 | Ajout de la gestion de Local et Global pour les options (au sens de | aspiwack |
| 2009-08-14 | Added profile.cmo in grammar.cma so that any functions in one of the | herbelin |
| 2009-08-14 | Tried to make F1 documentation tool working in CoqIDE. | herbelin |
| 2009-08-13 | Death of "survive_module" and "survive_section" (the first one was | herbelin |
| 2009-08-13 | Made unification patch 12268 even more ad hoc (if evars remain in a | herbelin |
| 2009-08-11 | Ensures that let-in's in arities of inductive types work well. Maybe not | herbelin |
| 2009-08-11 | Ajout des .annot dans le .gitignore. | aspiwack |
| 2009-08-11 | Fixed extra space in printing notation { x & P } + minor other things | herbelin |
| 2009-08-11 | Infix (r12268 continued) | herbelin |
| 2009-08-11 | Add support for "Infix ... := constr" instead of just "Infix ... := ref". | herbelin |
| 2009-08-11 | Relatively ad hoc fix to an ill-typed instantiation bug in type | herbelin |
