| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2012-03-20 | Reorganizing the structure of evarutil.ml (only restructuration, no | herbelin |
| 2012-03-20 | Turning proofs of well-ordering of lexicographic product transparent | herbelin |
| 2012-03-19 | More adaptations of pretyping/coercion to Program mode. | msozeau |
| 2012-03-19 | Fix bugs related to Program integration. | msozeau |
| 2012-03-19 | Hopefully complying with camlp5 < 6.00 syntax | herbelin |
| 2012-03-19 | Bug 2709: Duplication in coqdoc index entries | pboutill |
| 2012-03-19 | RefMan: Environment variables description update | pboutill |
| 2012-03-19 | Fixes bug: #2692 (Arguments/simpl off by 1) | gareuselesinge |
| 2012-03-19 | Arguments/simpl: allow ! even on non fixpoints | gareuselesinge |
| 2012-03-18 | Yet another subtlety with bug 2732: when several grammar rules of a | herbelin |
| 2012-03-18 | Removing redundant entry int_nelist and removing extra space when | herbelin |
