| Age | Commit message (Expand) | Author |
|---|
| 2009-07-09 | Correction bug 2134. | soubiran |
| 2009-07-08 | Fixed bug #2116 ("simpl" created ill-typed term while accepting | herbelin |
| 2009-07-08 | Don't use recent ocaml tolerance for pattern "ProjectVar _" when | herbelin |
| 2009-07-08 | Simplify addition of hints to a hint_db. Rebuild the dnet associated | msozeau |
| 2009-07-08 | 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-07 | Jolification : tentative de supprimer les "( evd)" et associés qui | aspiwack |
| 2009-07-06 | change in the order of unification constraints solving (for canonical structu... | amahboub |
| 2009-07-04 | repport of commit r12221 | jforest |
| 2009-07-01 | Support for binding Coq root read-only in -R option | herbelin |
| 2009-06-30 | Add new variants of [rewrite] and [autorewrite] which differ in the | msozeau |
| 2009-06-29 | Miscellaneous practical commits: | herbelin |
| 2009-06-29 | Fix bug introduced by last revision, subtac_cases was returning the | msozeau |
| 2009-06-28 | 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-26 | 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-22 | 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-18 | 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-17 | Fallback on not using [fix_proto] if the right imports aren't there, the | msozeau |
| 2009-06-16 | Reimplementation of leibniz rewrite to control the instantiation of the | msozeau |
| 2009-06-15 | Allow anonymous instances again, with syntax [Instance: T] where T | msozeau |
| 2009-06-13 | Correct typo: -noglob takes no argument. | msozeau |
| 2009-06-11 | 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-10 | Accept more Unicode symbols | glondu |
| 2009-06-10 | Use the projections for reflexivity, symmetry and transitivity proofs to | msozeau |
| 2009-06-09 | Correct handling of the initial existentials from the goal and the ones | msozeau |
| 2009-06-08 | 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-07 | 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-06 | 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 |
