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
*
congruence now knows about _ -> _
corbinea
2008-02-21
*
Petits oublis dans Makefile.doc
notin
2008-02-20
*
added products and sorts as possible heads for canonical structures
corbinea
2008-02-19
*
fixed pp for declarative mode
corbinea
2008-02-19
*
Petite correction suite à la révision 10571
notin
2008-02-18
*
Ajout de caractères unicode reconnus apr le lexer
notin
2008-02-18
*
Patch bug #1799
soubiran
2008-02-15
*
Suppression d'un include et de 2 variables inutiles
notin
2008-02-15
*
Suspension de l'introduction de delta dans apply : certaines contribs
herbelin
2008-02-14
*
Plongement de doc/Makefile dans la nouvelle architecutre des Makefile
notin
2008-02-14
*
Bug de Coqdoc avec l'option -R
notin
2008-02-14
*
Some bad emacs messup that was commited...
msozeau
2008-02-14
*
Reconnaissance des tokens dans les notations (suite à la revision r10562)
notin
2008-02-14
*
Added default canonical structures (see example in test-suite)
corbinea
2008-02-14
*
Backtrack changes on eauto, move specialized version of eauto in
msozeau
2008-02-14
*
Move class_setoid to class_tactics.
msozeau
2008-02-13
*
Debugging of the class_setoid tactic and eauto. Prepare for move from
msozeau
2008-02-13
*
Correction du bug #1512
notin
2008-02-13
*
Implement KEEP_ML4_PREPROCESSED option in build system
lmamane
2008-02-13
*
Implement NO_RECALC_DEPS option in build system
lmamane
2008-02-13
*
Suppression de l'option -glob-from de Coqdoc: les globalisations sont
notin
2008-02-13
*
Essai de prise en compte de delta dans unify_0 (même sur termes non clos).
herbelin
2008-02-13
*
Correction de ce qui semble être un petit bug dans la gestion de la
herbelin
2008-02-13
*
Correction d'un bug de clear
notin
2008-02-11
*
Fixing bug 1795 (occur check was not correctly done)
herbelin
2008-02-10
*
suppression code mort oublié lors du commit 10495
herbelin
2008-02-10
*
Granting wish 1794 (the name provided in the "using" clause of the
herbelin
2008-02-10
*
Backport Program Instance into Instance. Proper early error message if
msozeau
2008-02-10
*
Proposal of a nice notation for constructors xI and xO of type positive
letouzey
2008-02-10
*
Major revision: use of Function, including some non-structural ones
letouzey
2008-02-10
*
Major revision of FSetAVL: more Function, including some non-structural ones
letouzey
2008-02-09
*
Solde de code mort et petites optimisations sur lesquels je suis
herbelin
2008-02-09
*
Fix the clrewrite tactic, change Relations.v to work on relations in Prop
msozeau
2008-02-09
*
misc improvements
letouzey
2008-02-08
*
Documentation of CHANGES and refman doc for the implicit argument binder
msozeau
2008-02-08
*
better comments in FMapInterface
letouzey
2008-02-08
*
better comments in FSetInterface
letouzey
2008-02-08
*
Change implementation of resolution for typeclasses to use a customized
msozeau
2008-02-08
*
Add more information to IllFormedRecBody exceptions, to show the exact
msozeau
2008-02-08
*
Move generally useful definition of nf_evar on contexts to evarutil.
msozeau
2008-02-08
*
Add printer for Pp.std_ppcmds...
msozeau
2008-02-08
*
New "Preterm [ of id ] " command to show the preterm before giving it to
msozeau
2008-02-08
*
Backport code from command.ml to subtac_command.ml for definining
msozeau
2008-02-08
*
more complete FSets.v
letouzey
2008-02-08
*
updates concerning FSets
letouzey
2008-02-08
*
one forgotten compatibility lemma
letouzey
2008-02-08
*
Oubli dans r10524
notin
2008-02-08
*
Correction d'un bug de Coqdoc + ajout de Include dans les mots clés reconnus...
notin
2008-02-08
*
Mise en place d'une toute petite amélioration de l'unification de
herbelin
2008-02-07
*
Suite 10518
herbelin
2008-02-06
[next]