coq - The formal proof system

Age	Commit message (Expand)	Author
2008-07-07	- Improve [Context] vernacular to allow arbitrary binders, not just	msozeau
2008-07-04	Fixes in handling of implicit arguments:	msozeau
2008-05-11	- Cleanup parsing of binders, reducing to a single production for all	msozeau
2008-04-01	Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient	herbelin
2008-03-28	- Second pass on implementation of let pattern. Parse "let ' par [as x]?	msozeau
2008-03-27	Various fixes on typeclasses:	msozeau
2008-03-23	Fix a bug found by B. Grégoire when declaring morphisms in module	msozeau
2008-03-08	Fix bugs that were reopened due to the change of setoid	msozeau
2008-03-06	Syntax changes in typeclasses, remove "?" for usual implicit arguments	msozeau
2008-02-06	Fix obligations not being discharged due to new definition of complement.	msozeau
2008-02-03	Add new files theories/Program/Basics.v and theories/Classes/Relations.v	msozeau
2008-01-30	Support for occurences and 'in' in class_setoid, work on corresponding tactic...	msozeau
2008-01-18	Fix bug #1778, better typeclass error messages. Move Obligations Tactic to a ...	msozeau
2008-01-18	Change notation for setoid inequality, coerce objects before comparing them. ...	msozeau
2008-01-17	Fix Makefile bug, using .v instead of .vo and document SetoidDec.v	msozeau
2008-01-07	Remove spurious .d, better tactics.	msozeau
2008-01-04	Add partial setoids in theories/Classes, add SetoidDec class for setoids with...	msozeau