| Age | Commit message (Expand) | Author |
|---|
| 2011-06-18 | 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-17 | 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-16 | refman nsatz | pottier |
| 2011-06-16 | Tests de nsatz avec la geometrie | pottier |
| 2011-06-15 | git rebase -i mess consequence | pboutill |
| 2011-06-14 | 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-13 | 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-12 | 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-11 | Coqide now need lablgtk2.14.0 | pboutill |
| 2011-06-10 | 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-09 | More fixes in pruning/restriction of evars during unification. | msozeau |
| 2011-06-08 | Make Notation works with anonymous-level "Type". | herbelin |
| 2011-06-08 | Fixes in pruning in unification. | msozeau |
| 2011-06-07 | Fix bug #2399 in Program: used to build an ill-formed term due to a de Bruijn... | msozeau |
| 2011-06-07 | Fix bug #2335, fail if the search for reflexivity/symmetry/transitivity proof... | msozeau |
| 2011-06-07 | Catch AbstractionOverMeta as a unification failure in precatchable_exception. | msozeau |
| 2011-06-07 | Fix bug #2415: warn when closing modules or sections and some obligations are... | msozeau |
| 2011-06-07 | Fixed bug #2398: destruct ex2/sig2/sigT2 in Program, patch by Paolo Herms. | msozeau |
| 2011-06-07 | - Fix restrict_hyps to not allow filtering on a variable required to typechec... | msozeau |
