coq - The formal proof system

Age	Commit message (Expand)	Author
2008-12-10	Bug in 11662 (did not notice that dp_zenon.mll should be modified instead of	herbelin
2008-12-09	About "apply in":	herbelin
2008-12-04	Correct handling of defined methods (let-ins) in instance declarations.	msozeau
2008-11-27	fixed non-exhaustive pattern matching	barras
2008-11-24	amelioration mineur du comportement de Function	jforest
2008-11-23	first attempt to allow Function to deal with dependent pattern matching. This...	jforest
2008-11-22	Fixed bug in VernacExtend printing + missing vernacular printing rules +	herbelin
2008-11-20	correction of bug #2002	jforest
2008-11-09	f_equal : solve an inefficiency issue (apply vs. simple apply)	letouzey
2008-11-09	better fix for #1931 by using sort_of	letouzey
2008-11-09	More factorization of inductive/record and typeclasses: move class	msozeau
2008-11-07	Add the ability to give a specific tactic to solve each obligation in	msozeau
2008-11-06	Cosmetic: no more whitespace at end of lines in extraction files	letouzey
2008-11-05	Move Record desugaring to constrintern and add ability to use notations	msozeau
2008-11-05	Suite commit 11539 sur notation Record dans (Co)Inductive (MAJ	herbelin
2008-11-05	Nouvelle syntaxe pour écrire des records (co)inductifs :	aspiwack
2008-11-05	Better extraction renaming phase (fix #1914 plus other non-reported bugs)	letouzey
2008-10-26	Fixes and refinements regarding occurrence selection:	herbelin
2008-10-26	adding an option Function_raw_tcc to Function	jforest
2008-10-23	Fix bug #1977 by allowing the [apply] variants to take an [open_constr]	msozeau
2008-10-23	Open notation for declaring record instances.	msozeau
2008-10-23	Generalized implementation of generalization.	msozeau
2008-10-22	Affichage des notations récursives:	herbelin
2008-10-21	warning message when a qualid to extract can be both a module or a cst	letouzey
2008-10-19	Suite 11472	herbelin
2008-10-16	Extraction of Module with eq = ... : fix for bug #1853	letouzey
2008-10-16	Extraction of mutual types with alias: fix for bug #1965	letouzey
2008-10-16	Attempt to clarify Extract_env.extract_seb_spec	letouzey
2008-10-15	Report des commits 11417 et 11437 de la v8.2	soubiran
2008-10-11	Backporting 11445 from 8.2 to trunk (negative conditions in	herbelin
2008-10-03	Minor fixes related to coqdoc and --interpolate and the dependent	msozeau
2008-09-25	Partial fix for bug #1948: recompute order of dependencies between	msozeau
2008-09-15	Report improvements in Equations to the dependent elimination tactic:	msozeau
2008-09-15	Fix bug #1943 and restrict the inference optimisation of Program to	msozeau
2008-09-14	In manual implicit arguments mode, do not enrich implicits	msozeau
2008-09-14	Fix bug #1931 by searching for a sort after doing beta,iota,delta-	msozeau
2008-09-14	Fix bug #1936: uncaught exception due to undefinable exceptions.	msozeau
2008-09-14	Fix bug #1940: uncaught exception when searching for a type class.	msozeau
2008-09-13	Finish debugging the unification machinery in [Equations]. Do the _comp	msozeau
2008-09-12	Add a type argument to letin_tac instead of using casts and recomputing	msozeau
2008-09-11	Add enough information to correctly globalize recursive calls in inductive and	msozeau
2008-09-11	Some more debugging of [Equations], unification still not perfect.	msozeau
2008-09-10	profondeur maximale	filliatr
2008-09-07	Check [Equations] patterns are for the right function.	msozeau
2008-09-07	Add the ability to declare [Hint Extern]'s with no pattern.	msozeau
2008-09-07	Fixes in typeclasses resolution. Avoid reducing instances types before	msozeau
2008-09-07	More debugging of [Equations], now able to discharge even the heavily	msozeau
2008-09-07	Better handling of the opacity of proof obligations, add the possibility of	msozeau
2008-09-03	Better handling of recursive Equations definitions... still not perfect.	msozeau
2008-09-03	Fix bug #1935, reworking the reflexivity, symmetry... tactics to use	msozeau