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
*
Typo affichage "simple apply"
herbelin
2008-04-01
*
Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient
herbelin
2008-04-01
*
Ajout "simple apply" et "simple eapply" pour apply sans unfold
herbelin
2008-04-01
*
Finish enhancemenent of return clause inference from tycons, integrating
msozeau
2008-04-01
*
Enhance handling of parameters in typeclass constraints: permit to specify an...
msozeau
2008-04-01
*
Add option to set the opacity of obligations to transparent, to be able
msozeau
2008-04-01
*
Correction du bug #1819
notin
2008-04-01
*
- Fix for rewriting under dependent products.
msozeau
2008-03-31
*
Suite commit 10730: MAJ xlate.ml
herbelin
2008-03-30
*
Modifications diverses et variées :
herbelin
2008-03-30
*
Ajout d'abbréviations/notations paramétriques
herbelin
2008-03-30
*
Fix test-suite files, change conflicting notation "->rel" and the others
msozeau
2008-03-29
*
Improve error handling and messages for typeclasses.
msozeau
2008-03-28
*
- Second pass on implementation of let pattern. Parse "let ' par [as x]?
msozeau
2008-03-28
*
Correction du bug 1816 (ajout d'un lemme dans Znat) et suppression
notin
2008-03-28
*
- notations &&& and ||| equivalent to andb and orb,
letouzey
2008-03-27
*
Various fixes on typeclasses:
msozeau
2008-03-27
*
Diverses petites modifs dans la test-suite:
notin
2008-03-26
*
Bug dans la gestion des dépendances vers les .ml
notin
2008-03-26
*
Correction du bug #1814 (trunk et v8.1) + améliorations dans coqdep et coq_m...
notin
2008-03-26
*
Correction d'un bug sur Import/Export : ces fonctionnalites sont gerees en-de...
soubiran
2008-03-26
*
Prise en compte des dépendances des .ml
notin
2008-03-25
*
Correction de bugs relatifs a la compostion des substitutions
soubiran
2008-03-25
*
Correction d'un bug dans la gestion des 'Declare ML Module'
notin
2008-03-25
*
Interpret patterns for hypotheses types in match goal in type_scope (if not a
msozeau
2008-03-25
*
Finish fix in command where we still lost information on what was a type
msozeau
2008-03-24
*
Fix examples in Program documentation and add comindexes for the various
msozeau
2008-03-23
*
Fix a bug found by B. Grégoire when declaring morphisms in module
msozeau
2008-03-23
*
Nettoyage Wf.v et unification (suite remarques faites sur cocorico)
herbelin
2008-03-23
*
Commit d'une preuve de l'axiome d'Archimède qui traînait dans mes placards.
herbelin
2008-03-23
*
Une passe sur les réels:
herbelin
2008-03-23
*
CoqIDE default font set to monospace so as indentation to be meaningful
herbelin
2008-03-23
*
Compatibility fixes, backtrack on definitions of reflexive,
msozeau
2008-03-22
*
One more AVL reorganisation: separate pure functions from proofs + functional...
letouzey
2008-03-21
*
Correct bug introduced in r10589, where we lost information that
msozeau
2008-03-21
*
Some "if then else" instead of orb and andb, in order to vm_compute lazily
letouzey
2008-03-21
*
Add a flag to control rewriting under lambdas. Otherwise makes some
msozeau
2008-03-20
*
Installation des .vo nécessaire à BigQ
notin
2008-03-20
*
Correction d'un bug sur les modules de la forme:
soubiran
2008-03-20
*
still some useless invariants in FSetAVL
letouzey
2008-03-20
*
some references to IntMap forgotten in last commit
letouzey
2008-03-19
*
migration of the old IntMap library from StdLib to a user contrib (Cachan/Int...
letouzey
2008-03-19
*
Coq.Relations.Relations can move back to its short name
letouzey
2008-03-19
*
Do another pass on the typeclasses code. Correct globalization of class
msozeau
2008-03-19
*
tactique gappa
filliatr
2008-03-19
*
Various improvements of coqdep, resulting in a big speedup
letouzey
2008-03-19
*
Implementation of rewriting under lambdas. Tested on exists only.
msozeau
2008-03-18
*
Added a function to rebuild an elim scheme from elim_scheme_info. Will
courtieu
2008-03-18
*
Hint for Debian users.
glondu
2008-03-18
*
improved the implementation of rtree
barras
2008-03-18
[next]