index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
...
*
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
*
Use Type instead of Set.
msozeau
2009-06-02
*
Backtrack on experimental unification with sort variables: it requires
msozeau
2009-06-02
*
Fix script file using the "Manual Implicit" flag.
msozeau
2009-06-02
*
## Lines starting with '## ' will be removed from the log message.
msozeau
2009-06-01
*
Change unification with sort constraints to not use the kernel
msozeau
2009-06-01
*
Prevent automatic inference of implicit arguments when the auto flag is
msozeau
2009-06-01
*
Fix extract hyps to correctly discharge all hyps as described by keep
msozeau
2009-05-29
*
Properly catch sort constraint inconsistency exception in
msozeau
2009-05-28
*
Adapted the emacs mode to font-lock. Re-using code from ProofGeneral.
courtieu
2009-05-28
[prev]
[next]