coq - The formal proof system

Age	Commit message (Expand)	Author
2011-05-05	Merge branch 'subclasses' into coq-trunk	msozeau
2011-04-29	Typo in test InitSyntax.out	herbelin
2011-04-28	Fixing an "apply -> ... in hyp" bug (the hyp was considered as a fixed	herbelin
2011-04-28	Fixed notation printing bug when curly brackets are involved (requests	herbelin
2011-04-27	Fixing output of Notations2.v test messed up in r14060	herbelin
2011-04-25	Fixing and completing interpretation of let's in notations for iterated binders.	herbelin
2011-04-15	Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".	herbelin
2011-04-13	Revert "Add [Polymorphic] flag for defs"	msozeau
2011-04-13	- Do not make constants with an assigned type polymorphic (wrong unfoldings).	msozeau
2011-04-13	Add [Polymorphic] flag for defs	msozeau
2011-04-08	Applying and reworking Tom Prince's patch for test-suite/failure/universes2.v	herbelin
2011-04-08	Fixing multiple printing bugs with "Notation f x := ..."	herbelin
2011-03-31	Did that adding a rule for printing applications as "f(x)" works.	herbelin
2011-03-16	Remove some weird syntax "fun ... ," that used to be accepted (cf r13876)	letouzey
2011-03-16	Adapt test-suite/output/Extraction_matchs_2413 to new indentation of extraction	letouzey
2011-03-13	Fix inductive_template building ill-typed evars, and update test-suite scripts	msozeau
2011-03-05	Starting being more explicit on the reasons why module subtyping fails.	herbelin
2011-03-05	Improved define_evar_as_lambda which was creating an unrelated new evar	herbelin
2011-02-22	Try to fix the behavior of clenv_missing used when declaring hints	letouzey
2011-02-21	Some fixes of the test-suite scripts	letouzey
2011-02-21	Fix test-suite script.	msozeau
2011-02-10	MacOS compatibility	pboutill
2011-02-08	Correct handling of existential variables when multiple different	msozeau
2011-01-27	test-suite/Makefile: add a rule to build all_stdlib.v (for the bench)	glondu
2011-01-25	Add a test for sorting all universes of stdlib	glondu
2011-01-11	Add "Print Sorted Universes"	glondu
2011-01-07	Fixing an uncaught exception bug with use of vmcast	herbelin
2010-12-23	Remove the two-argument variant of "decide equality"	glondu
2010-12-21	Extraction: avoid type-unsafe optimisation of pattern-matchings (fix #2413)	letouzey
2010-12-19	Fixing bug #2454: inversion predicate strategy for inferring the type	herbelin
2010-12-04	Fixing bug #2448 (wrongly-scoped alpha-renaming in notations).	herbelin
2010-12-03	Fixing bug using explictly declared implicit arguments in inductive arities.	herbelin
2010-12-02	Fixing a bug introduced in r12304 (move of interpretation of	herbelin
2010-11-19	SearchAbout: who has never been annoyed by the [ ] syntax ?	letouzey
2010-10-31	An experimental support for open constrs in hints and in "using"	herbelin
2010-10-16	Fix missing -coqlib argument to coqdep in test-suite	glondu
2010-10-12	Adding test-case for bug #2362, which uses HO unification during	msozeau
2010-10-12	Fix bug #2393: allow let-ins inside telescopes (only fails when there's	msozeau
2010-10-11	Backporting r13521 from branch 8.3 to trunk (fixing bug #2406, looping	herbelin
2010-10-07	test-suite: fix success/unification.v	glondu
2010-10-06	test-suite: fix output/Existentials.out	glondu
2010-10-05	test-suite: fix success/Typeclasses.v	glondu
2010-10-05	test-suite: fix success/AdvancedCanonicalStructure.v	glondu
2010-10-05	Export definition of type implicits_list for contribs + fixed a	herbelin
2010-10-05	test-suite: use unified diff output and use expected output as reference	glondu
2010-10-04	Fixing bugs in previous commits about implicit arguments:	herbelin
2010-10-03	Test for non-regression of the display bug fixed in r13486.	herbelin
2010-10-03	Added multiple implicit arguments rules per name.	herbelin
2010-10-03	Making display of various informations about constants more modular:	herbelin
2010-09-30	Improve handling of metas as evars in unification (patch by Hugo)	letouzey