coq - The formal proof system

Age	Commit message (Expand)	Author
2014-09-19	Fixing bug #3646.	Pierre-Marie Pédrot
2014-09-18	mltop: when a plugin is loaded store its full path in the summary	Enrico Tassi
2014-09-17	Be more conservative and keep the use of eq_constr in pretyping/ functions.	Matthieu Sozeau
2014-09-17	Fix bug #3593, making constr_eq and progress work up to	Matthieu Sozeau
2014-09-17	Revert specific syntax for primitive projections, avoiding ugly	Matthieu Sozeau
2014-09-16	Undo prints only if coqtop \|\| emacs	Enrico Tassi
2014-09-16	better error message	Enrico Tassi
2014-09-15	Rework typeclass resolution and control of backtracking.	Matthieu Sozeau
2014-09-13	Providing a -type-in-type option for collapsing the universe hierarchy.	Hugo Herbelin
2014-09-12	Uniformisation of the order of arguments env and sigma.	Hugo Herbelin
2014-09-12	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin
2014-09-11	Add a flag for restricting resolution of typeclasses to	Matthieu Sozeau
2014-09-10	Fix categorization of recursive inductives.	Matthieu Sozeau
2014-09-10	Fixing localisation of tactic errors (my mistake in himsg.ml essentially).	Hugo Herbelin
2014-09-10	VernacExtend does not dispatch on type anymore.	Pierre-Marie Pédrot
2014-09-09	Load Prelude.vi if not Prelude.vo is found (Close: 3595)	Enrico Tassi
2014-09-09	Undo: if the ui is coqtop (command line) then Undo is not part of the doc.	Enrico Tassi
2014-09-09	toploop plugins taken into account when printing --help (close: 3535)	Enrico Tassi
2014-09-08	Removing dead code relative to the XML plugin.	Pierre-Marie Pédrot
2014-09-08	Parsing of Type@{max(i,j)}.	Matthieu Sozeau
2014-09-07	Fixing bug #3492.	Pierre-Marie Pédrot
2014-09-06	Renaming goal-entering functions.	Pierre-Marie Pédrot
2014-09-04	More explicit printing in Himsg.	Pierre-Marie Pédrot
2014-09-04	Commands like [Inductive > X := … \| … \| …] raise an error message inste...	Arnaud Spiwack
2014-09-04	Remove [Infer] option of records.	Arnaud Spiwack
2014-09-04	Type definitions with [Variant] don't generate inductive schemes by default.	Arnaud Spiwack
2014-09-04	Type definitions [Variant] and [Record] really don't accept the wrong kind of...	Arnaud Spiwack
2014-09-04	Types declared as Variants really do not accept recursive definitions.	Arnaud Spiwack
2014-09-04	Print [Variant] types with the keyword [Variant].	Arnaud Spiwack
2014-09-03	Print error messages with more hidden information based on α-equivalence .	Arnaud Spiwack
2014-09-03	Additional entry tactic_arg in Print Grammar tactic.	Pierre-Marie Pédrot
2014-09-02	coqworkmgr	Enrico Tassi
2014-08-31	Getting rid of atomic tactics in Tacenv.	Pierre-Marie Pédrot
2014-08-31	Moving code of tactic interpretation from Tacenv to Vernacentries.	Pierre-Marie Pédrot
2014-08-30	Simplify even further the declaration of primitive projections,	Matthieu Sozeau
2014-08-29	Fixing commit 50237af2.	Pierre-Marie Pédrot
2014-08-29	Fix bug when defining primitive projections mixing defined and abstracts fields.	Matthieu Sozeau
2014-08-28	Fixing bug #3528.	Pierre-Marie Pédrot
2014-08-28	Change the way primitive projections are declared to the kernel.	Matthieu Sozeau
2014-08-25	Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possible	Matthieu Sozeau
2014-08-25	Fixing the essence of naming bug #3204: use same strategy for naming	Hugo Herbelin
2014-08-25	Prerequisite to fix stm test-suite when not in -local	Pierre Boutillier
2014-08-23	Fixing bug #3533.	Pierre-Marie Pédrot
2014-08-22	Move UnsatisfiableConstraints to a pretype error.	Matthieu Sozeau
2014-08-18	Reorganisation of intropattern code	Hugo Herbelin
2014-08-18	Reorganization of tactics:	Hugo Herbelin
2014-08-18	Moving the TacAlias node out of atomic tactics.	Pierre-Marie Pédrot
2014-08-18	Moving the TacExtend node from atomic to plain tactics.	Pierre-Marie Pédrot
2014-08-16	Removing documentation related to the deprecated State machinery.	Pierre-Marie Pédrot
2014-08-14	Fix program using an the unsubstituted type of the original obligation	Matthieu Sozeau