| Age | Commit message (Expand) | Author |
|---|
| 2012-04-12 | make otags only relies on otags | pboutill |
| 2012-04-12 | "A -> B" is a notation for "forall _ : A, B". | pboutill |
| 2012-04-12 | Coqide minor enhancements | pboutill |
| 2012-04-12 | lib directory is cut in 2 cma. | pboutill |
| 2012-04-12 | Repair two tests | letouzey |
| 2012-04-12 | CHANGES: adapt after backport of some features to 8.4 | letouzey |
| 2012-04-12 | remove plugins/subtac/subtac.ml reintroduced by mistaked in a previous commit | letouzey |
| 2012-04-11 | Added a reset button for CoqIDE colors | ppedrot |
| 2012-04-11 | Added a background color configuration option in CoqIDE. | ppedrot |
| 2012-04-07 | Fixing the "capture" check newly introduced in r15122 when | herbelin |
| 2012-04-06 | Unifying the different procedures for interning binders. | herbelin |
| 2012-04-06 | Fixing a few bugs (see #2571) related to interpretation of multiple binders | herbelin |
| 2012-04-06 | Removing Dhyp from debugger. | herbelin |
| 2012-04-05 | Shortcuts and optimizations of comparisons | xclerc |
| 2012-04-05 | Relax uniform inheritance condition | gareuselesinge |
| 2012-04-05 | Speedup free_vars_and_rels_up_alias_expansion (evarconv) | gareuselesinge |
| 2012-04-04 | Reversed colour highlight in CoqIDE | ppedrot |
| 2012-03-30 | Typo in a message. | aspiwack |
| 2012-03-30 | Added a command "Unfocused" which returns an error when the proof is | aspiwack |
| 2012-03-30 | info_trivial, info_auto, info_eauto, and debug (trivial|auto) | letouzey |
| 2012-03-30 | Remove code of obsolete tactics : superauto, autotdb, cdhyp, dhyp, dconcl | letouzey |
| 2012-03-28 | A revolution has come: CoqIDE, now in color. Fixes bug #2704 btw. | ppedrot |
| 2012-03-26 | Adapt the checker after commit 15080 | letouzey |
| 2012-03-26 | Unification: Fixing bug in materialize_evar (spotted by MathClasses). | herbelin |
| 2012-03-26 | Slight change in the semantics of arguments scopes: scopes can no | herbelin |
| 2012-03-26 | Fixing printing level of Utf8 equivalent for ->. | herbelin |
| 2012-03-26 | Fixing deactivation of scope at printing time in the body of a | herbelin |
| 2012-03-26 | Unification: Added a heuristic to solve problems of the form | herbelin |
| 2012-03-26 | Module names and constant/inductive names are now in two separate namespaces | letouzey |
| 2012-03-23 | Fix the test-suite by removing any Reset in the scripts | letouzey |
| 2012-03-23 | Documentation of last commit concerning Backtracking | letouzey |
| 2012-03-23 | A unified backtrack mechanism, with a basic "Show Script" as side-effect | letouzey |
| 2012-03-23 | Remove undocumented command "Delete foo" | letouzey |
| 2012-03-23 | Remove old proof-managment commands Suspend/Resume | letouzey |
| 2012-03-23 | Little bug in r15061 leading to unusable debug mode. | herbelin |
| 2012-03-22 | Univ: enforce_leq instead of enforce_geq for more uniformity | letouzey |
| 2012-03-22 | Univ: switch the order of int and dir_path in UniverseLevel.Level | letouzey |
| 2012-03-22 | Update of .gitignore (via a regexp g_*.ml) | letouzey |
| 2012-03-22 | evarconv: MaybeFlex/MaybeFlex case infers more Canonical Structures | gareuselesinge |
| 2012-03-21 | Ppvernac: nicer printing of proof delimiters { ... } | letouzey |
| 2012-03-21 | Pfedit: avoid Undoing too much | letouzey |
| 2012-03-20 | Fix interface of resolve_typeclasses: onlyargs -> with_goals: | msozeau |
| 2012-03-20 | Arranged for the desirable behaviour that bullets do not see beyond braces. | aspiwack |
| 2012-03-20 | Fixing bug #2724 (using notations with binders in cases patterns | herbelin |
| 2012-03-20 | Fixing alpha-conversion bug #2723 introduced in r12485-12486. | herbelin |
| 2012-03-20 | Continuing r15045-15046 and r15055 (fixing bug #2732 about atomic | herbelin |
| 2012-03-20 | Use a careful analysis of dependencies in restricting instances to | herbelin |
| 2012-03-20 | Force Check (which, from 8.4beta, accepts unresolved evars) to however | herbelin |
| 2012-03-20 | Unification: when matching "?n[...,(C u1..un),...] = C u1..un" keep a | herbelin |
| 2012-03-20 | Generalized the use of evar candidates in type inference unification: | herbelin |
