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
*
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
*
Ajout d'un printer modulaire pour les constr. C'est-à-dire une fonction
aspiwack
2009-05-28
*
Fix implicit args code so that declarations are added for all
msozeau
2009-05-27
*
Populate the sort constraints set correctly during unification. Add a
msozeau
2009-05-27
*
Stop using a "Manual Implicit Arguments" flag and support them as soon
msozeau
2009-05-27
*
Ajout d'une fonction Lexer.remove_keyword pour libérer un keyword dans
aspiwack
2009-05-27
*
=?utf-8?q?D=C3=A9sinterdiction=20de=20GDELETE=5FRULE=20dans=20pcoq.ml4.=20Mal...
aspiwack
2009-05-27
*
sane behaviour for copy/paste operations (the code is still insane, though)
vgross
2009-05-27
*
keeping interface synch'ed
vgross
2009-05-27
*
dead code pruning
vgross
2009-05-27
*
Fix de Bruijn lifting bug appearing when we match on multiple terms with
msozeau
2009-05-26
*
ocamldebug-coq: add some forgotten -I
letouzey
2009-05-26
*
Temporary fixes in unification:
msozeau
2009-05-24
*
Moved and completed the history of Coq versions from the
herbelin
2009-05-24
*
A try at using sort variables during unification. Instead of refreshing
msozeau
2009-05-23
*
Many fixes in unification:
msozeau
2009-05-20
*
- Fixing declarative mode in presence of high use of Change_evars nodes
herbelin
2009-05-20
*
Fix in canonical structure resolution: [check_conv_record] may return
msozeau
2009-05-19
*
Remove camlp4-specific exception handling
msozeau
2009-05-19
*
Minor unification changes:
msozeau
2009-05-18
*
- Allowing multiple calls to tactic fix with automatic generation of
herbelin
2009-05-17
*
(Tentative to) add Canonical Structure resolution to the regular
msozeau
2009-05-16
*
Minor fixes in typeclasses:
msozeau
2009-05-16
*
Support for definition hooks in subtac.
msozeau
2009-05-16
*
Fix to my last notation patch: now fixpoint are correctly handled
vsiles
2009-05-13
[next]