| Age | Commit message (Expand) | Author |
|---|
| 2009-09-23 | Ltac doc: only variables are accepted as message_token | glondu |
| 2009-09-22 | Add the option to automatically introduce variables declared before the | msozeau |
| 2009-09-22 | Better use of transparency information for local hypotheses: | msozeau |
| 2009-09-21 | Update link to "Recursive Make Considered Harmful" | glondu |
| 2009-09-20 | Only one "in" clause in "destruct" even for a multiple "destruct". | herbelin |
| 2009-09-20 | Add "case as/in/using" and temporary "destruct" with n args. | herbelin |
| 2009-09-18 | micromega: better handling of exponentiation + correction of test-suite termi... | fbesson |
| 2009-09-18 | - Fixed a bug in checking that implicit arguments are all correctly | herbelin |
| 2009-09-17 | Replace call to where_in_path by find_file_in_path in "Locate File" | glondu |
| 2009-09-17 | Replace unprotected call to where_in_path by find_file_in_path | glondu |
| 2009-09-17 | Remove useless MonoList.v | glondu |
| 2009-09-17 | Remove useless Liboject.export_function field | glondu |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-09-17 | Fix typos in comments | glondu |
| 2009-09-17 | Clarify documentation of ltac repeat | glondu |
| 2009-09-15 | - Tentatively made order-dependency wrt .vo files a full dependency | herbelin |
| 2009-09-15 | Fix compilation errors due to last commit. | msozeau |
| 2009-09-15 | Dont't forget to update the state or an obligation tactic assignment may | msozeau |
| 2009-09-15 | Fixed compilation error message which was no longer emacs-compliant since | herbelin |
| 2009-09-15 | Stop using [obligation_tactic] from Program.Tactics as the default | msozeau |
| 2009-09-14 | Backtrack on the forced discharge of type class variables introduced | msozeau |
| 2009-09-14 | removed the double-click / proof hiding association. | vgross |
| 2009-09-14 | tags refactoring | vgross |
| 2009-09-14 | - Addition of "Reserved Infix" continued. | herbelin |
| 2009-09-13 | - Inductive types in the "using" option of auto/eauto/firstorder are | herbelin |
| 2009-09-11 | Addendum to revision 12323; update Makefile.common after removal of | herbelin |
| 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 |
