| Commit message (Expand) | Author | Age |
|---|
| ... | |
| * | Use user-given implicits from the arity in inductive definitions. |  msozeau | 2009-07-08 |
| * | Reactivation of pattern unification of evars in apply unification, in |  herbelin | 2009-07-08 |
| * | Add heuristic based on non-linearity of evars to determine whether an | herbelin | 2009-07-08 |
| * | Fixed anomaly when trying to load non existing file starting with "./" or "../". | herbelin | 2009-07-08 |
| * | Fixing bug 2129 (evar introduced to remember an ambiguous projection | herbelin | 2009-07-08 |
| * | Completing support for F5=About by adding About to the state-preserving comma... | herbelin | 2009-07-08 |
| * | Jolification : tentative de supprimer les "( evd)" et associés qui |  aspiwack | 2009-07-07 |
| * | change in the order of unification constraints solving (for canonical structu... |  amahboub | 2009-07-06 |
| * | repport of commit r12221 |  jforest | 2009-07-04 |
| * | Support for binding Coq root read-only in -R option | herbelin | 2009-07-01 |
| * | Add new variants of [rewrite] and [autorewrite] which differ in the | msozeau | 2009-06-30 |
| * | Miscellaneous practical commits: | herbelin | 2009-06-29 |
| * | Fix bug introduced by last revision, subtac_cases was returning the | msozeau | 2009-06-29 |
| * | Raise an error and not an anomaly if a rewrite is attempted on a | msozeau | 2009-06-28 |
| * | Abstract the tycon by the matched terms when turning them into variables | msozeau | 2009-06-28 |
| * | Improve return predicate inference by making the return type dependent | msozeau | 2009-06-28 |
| * | propagation sur le trunk du commit 12101 |  soubiran | 2009-06-26 |
| * | Add doc for [Print Opaque Dependencies] and a better explanation for the | msozeau | 2009-06-26 |
| * | Correct treatment of dependent products in signatures: create the evars | msozeau | 2009-06-22 |
| * | Fixes for r12197, the refined evars were not returned in case fail_evar | msozeau | 2009-06-22 |
| * | documented a bug of pattern unification with metas |  barras | 2009-06-22 |
| * | made several occurrences of (eapply ...; eauto) not rely on the lack of patte... | barras | 2009-06-22 |
| * | Report de la révision #12200 (bug #2125) |  notin | 2009-06-22 |
| * | remove some unused functions (which are part of a soon-to-be obsolete |  vgross | 2009-06-22 |
| * | clearing unused functions | vgross | 2009-06-22 |
| * | Use more consistent resolution parameters in Program and regular typing | msozeau | 2009-06-18 |
| * | Fix "unsatisfiable constraints" error messages to include all the | msozeau | 2009-06-18 |
| * | Try typeclass resolution in coercion if no solution can be found to a | msozeau | 2009-06-18 |
| * | Fallback on not using [fix_proto] if the right imports aren't there, the | msozeau | 2009-06-17 |
| * | Reimplementation of leibniz rewrite to control the instantiation of the | msozeau | 2009-06-16 |
| * | Allow anonymous instances again, with syntax [Instance: T] where T | msozeau | 2009-06-15 |
| * | Correct typo: -noglob takes no argument. | msozeau | 2009-06-13 |
| * | Use a lazy value for the message in FailError, so that it won't be | msozeau | 2009-06-11 |
| * | Simplifying the call to print_no_goals and not calling it when no goal | herbelin | 2009-06-11 |
| * | When typing a non-dependent arrow, do not put the (anonymous) variable | msozeau | 2009-06-11 |
| * | Accept more Unicode symbols |  glondu | 2009-06-10 |
| * | Use the projections for reflexivity, symmetry and transitivity proofs to | msozeau | 2009-06-10 |
| * | Correct handling of the initial existentials from the goal and the ones | msozeau | 2009-06-09 |
| * | Do a fixpoint on the result of typeclass search to force the | msozeau | 2009-06-08 |
| * | Change in UI behaviour : proof folding is now done by double clicking. Delay is | vgross | 2009-06-08 |
| * | File forgotten in commit 12171. | herbelin | 2009-06-07 |
| * | Partial simplification of undo mechanism, relying only on Courtieu's | herbelin | 2009-06-07 |
| * | - Added two new introduction patterns with the following temptative syntaxes: | herbelin | 2009-06-07 |
| * | Makefile made compatible with Solaris 10 (bug #2078, continued - see | herbelin | 2009-06-06 |
| * | Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0 | herbelin | 2009-06-06 |
| * | Fixing bug #2106 ("match" compilation with multi-dependent constructor). | herbelin | 2009-06-06 |
| * | Very-small-step policy changes to the library. | herbelin | 2009-06-06 |
| * | Applying Ian Lynagh's documentation fixes patch (see bug #2112) | herbelin | 2009-06-06 |
| * | Ensure the precondition of the partial function [list_chop] holds | msozeau | 2009-06-03 |
| * | Adding a regression test about Bauer's example on coq-club of | herbelin | 2009-06-02 |
msozeau
herbelin
aspiwack
amahboub
jforest
soubiran
barras
notin
vgross
glondu