index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
Commit message (
Expand
)
Author
Age
*
contradict can now handle False hypothesis in the spirit of contradiction
letouzey
2008-04-09
*
Fix the last compilation problem
msozeau
2008-04-09
*
Fix compilation problem
msozeau
2008-04-09
*
- A little cleanup in Classes/*. Separate standard morphisms on
msozeau
2008-04-08
*
Renoncement à rationaliser les Hints "real" vis à vis de Rle/Rge et Rlt/Rgt :
herbelin
2008-04-06
*
Suite 10760
herbelin
2008-04-05
*
- Retour en arrière sur la capacité du nouvel apply à utiliser les
herbelin
2008-04-05
*
Minor fixes:
msozeau
2008-04-05
*
A file that can be loaded when a migration from Set to Type is desired
letouzey
2008-04-04
*
Correction problème de compil (blast.ml)
herbelin
2008-04-04
*
- Amélioration de la présentation de RIneq, même si un nettoyage des
herbelin
2008-04-04
*
New file FMapFullAVL containing the balancing proofs about FMapAVL:
letouzey
2008-04-03
*
Rework of FMapAVL inspired by recent changes of FSetAVL:
letouzey
2008-04-03
*
Minor fixes. Use expanded type in class_tactics for Morphism search, to
msozeau
2008-04-02
*
Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient
herbelin
2008-04-01
*
Correction du bug #1819
notin
2008-04-01
*
- Fix for rewriting under dependent products.
msozeau
2008-03-31
*
Modifications diverses et variées :
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
*
Interpret patterns for hypotheses types in match goal in type_scope (if not a
msozeau
2008-03-25
*
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
*
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
*
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
*
still some useless invariants in FSetAVL
letouzey
2008-03-20
*
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
*
Implementation of rewriting under lambdas. Tested on exists only.
msozeau
2008-03-18
*
Correct implementation of normalization of signatures using setoid
msozeau
2008-03-18
*
Add the possibility of specifying constants to unfold for typeclass
msozeau
2008-03-17
*
Removed unneeded tactics from RelationClasses. Use
msozeau
2008-03-16
*
Using the "relation" constant made some unifications fail in the new
msozeau
2008-03-16
*
Misc: Add test for bug 1704, now closed. Add usual syntax for lists in
msozeau
2008-03-16
*
Reorganize Program and Classes theories. Requiring Setoid no longer sets
msozeau
2008-03-16
*
Minor fixes on setoid rewriting. Now uses definitions of [relation] and
msozeau
2008-03-16
*
Reorganisation of FSetAVL (consequences of remarks by B. Gregoire)
letouzey
2008-03-15
*
Do a second pass on the treatment of user-given implicit arguments. Now
msozeau
2008-03-15
*
Suppress some warnings by writing ugly Coq.Relations.Relations in some .v
letouzey
2008-03-14
*
Add a missing morphism declaration that turns morphisms on R ==> R' to
msozeau
2008-03-09
*
Fix bugs that were reopened due to the change of setoid
msozeau
2008-03-08
[next]