| Commit message (Expand) | Author | Age |
|---|
| * | Zcompare.destr_zcompare subsumed by case Z.compare_spec |  letouzey | 2011-06-20 |
| * | Clean-up of Zcompare and Zorder | letouzey | 2011-06-20 |
| * | Arithemtic: more concerning compare, eqb, leb, ltb | letouzey | 2011-06-20 |
| * | Some simplifications in NZDomain | letouzey | 2011-06-20 |
| * | Add compatibility option "-compat 8.3". |  herbelin | 2011-06-20 |
| * | Fixing two typos introduced in r14217 and r14223 | herbelin | 2011-06-20 |
| * | Ensured that the transparency state is used when flag betaiota is on for apply. | herbelin | 2011-06-19 |
| * | Relaxed the constraint introduced in r14190 that froze the existing | herbelin | 2011-06-18 |
| * | Generalizing flag use_evars_pattern_unification into a flag | herbelin | 2011-06-18 |
| * | Activating flags betaiota by default for apply | herbelin | 2011-06-18 |
| * | r14204 and 14218 continued: completely removing test for bug #2490, | herbelin | 2011-06-18 |
| * | Partial backtrack on wrong r14204: bug #2490 still open. | herbelin | 2011-06-18 |
| * | The ad hoc version for first-order unification at toplevel of "?n args | herbelin | 2011-06-18 |
| * | Typo in CHANGES | herbelin | 2011-06-18 |
| * | add names of theorems in output |  jnarboux | 2011-06-18 |
| * | Customized accelerator maps for macos are globally installed (end to fix 2462) |  pboutill | 2011-06-17 |
| * | Fix 2516: Utf8 font in Coqide Command panel | pboutill | 2011-06-17 |
| * | Fix bug 2269, program typechecker not used in Instance conclusions |  msozeau | 2011-06-17 |
| * | refman nsatz |  pottier | 2011-06-16 |
| * | Tests de nsatz avec la geometrie | pottier | 2011-06-16 |
| * | git rebase -i mess consequence | pboutill | 2011-06-15 |
| * | Revert "Coqide now need lablgtk2.14.0" + Ide build system debugging | pboutill | 2011-06-14 |
| * | Making printing of backtick in Program reparsable (avoiding collision with "`(") | herbelin | 2011-06-14 |
| * | Regression files for bugs #2304 and #2490. | herbelin | 2011-06-14 |
| * | Fixing bug #2181 (Class mechanism can create dependencies over unnamed | herbelin | 2011-06-14 |
| * | A few comments and a dev file to summarize issues with unification | herbelin | 2011-06-13 |
| * | Added full pattern-unification on Meta for tactic unification. | herbelin | 2011-06-13 |
| * | Added a flag to restrict conversion in tactic unification on the | herbelin | 2011-06-13 |
| * | Another bug of Scheme Induction (generated names dep/nodep were swapped). | herbelin | 2011-06-13 |
| * | Fixing an anomaly in Scheme Induction. | herbelin | 2011-06-13 |
| * | Oups, typo in previous commit | herbelin | 2011-06-12 |
| * | Removed what looks like a (very old) useless f.o. unification pass | herbelin | 2011-06-12 |
| * | Added a new flag for freezing evars in tactic unification. Used this | herbelin | 2011-06-12 |
| * | Rather quick hack to avoid using notations involving "Type" when | herbelin | 2011-06-12 |
| * | Coqide now need lablgtk2.14.0 | pboutill | 2011-06-11 |
| * | Updated CHANGES (info, Show Script, rephrasing). | herbelin | 2011-06-10 |
| * | Moved allow_K to a unification flag | herbelin | 2011-06-10 |
| * | Fixing another bug with "_" intro pattern. | herbelin | 2011-06-10 |
| * | Fixing the "buggy" first_name and prepare multi-induction. | herbelin | 2011-06-10 |
| * | Made use of "_" in repeated use of intros_patterns work (with | herbelin | 2011-06-10 |
| * | Integrating onLastHypId into intro so that we can get the introduction | herbelin | 2011-06-10 |
| * | Call process_vernac_interp_error before calling Errors.print in | herbelin | 2011-06-10 |
| * | Coqide Menubar integration in MacOS | pboutill | 2011-06-10 |
| * | no more errors at _stubs.c.d generation | pboutill | 2011-06-10 |
| * | Menubar and toolbar in coqide using GtkUI & Gactions. | pboutill | 2011-06-10 |
| * | Revert "Check if recursive calls are guarded before printing "Proof completed"." | pboutill | 2011-06-10 |
| * | Fixes in pruning, do not fail if pruning is impossible due to typing constrai... | msozeau | 2011-06-10 |
| * | ring2, cring, nsatz avec type classe avec parametres plus notations | pottier | 2011-06-10 |
| * | More fixes in pruning/restriction of evars during unification. | msozeau | 2011-06-09 |
| * | Make Notation works with anonymous-level "Type". | herbelin | 2011-06-08 |
letouzey
herbelin
jnarboux
pboutill
msozeau
pottier