coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Seeing IntroWildcard as an action intro pattern rather than as a naming pattern	Hugo Herbelin	2014-09-30
*	Add syntax for naming new goals in refine: writing ?[id] instead of _	Hugo Herbelin	2014-09-30
*	Simplify evarconv thanks to new delta status of projections,	Matthieu Sozeau	2014-09-30
*	XML pretty printing for AST (work by François Poulain, project DoCoq)	Enrico Tassi	2014-09-29
*	Notation: option to attach extra pretty printing rules to notations	Enrico Tassi	2014-09-29
*	CoqIDE: new message to print AST	Enrico Tassi	2014-09-29
*	typo	Enrico Tassi	2014-09-29
*	do not explode if a plugin is not up to date on -help (Close: 3673)	Enrico Tassi	2014-09-29
*	Merging some functions from evarutil.ml/evd.ml.	Hugo Herbelin	2014-09-29
*	Printing evar instance in a more intuitive order.	Hugo Herbelin	2014-09-29
*	Restoring non-uniform delta on local and global constants in 2nd order	Hugo Herbelin	2014-09-29
*	Documenting option -type-in-type.	Hugo Herbelin	2014-09-29
*	Adding a test for bug #2428.	Pierre-Marie Pédrot	2014-09-29
*	Bug fixed.	Matthieu Sozeau	2014-09-29
*	Fix test-suite files	Matthieu Sozeau	2014-09-29
*	Fix printing of primitive record info.	Matthieu Sozeau	2014-09-29
*	In evarconv and unification, expand folded primitive projections to	Matthieu Sozeau	2014-09-29
*	Print information about primitive records (Print and About).	Matthieu Sozeau	2014-09-28
*	Keyed unification option, compiling the whole standard library	Matthieu Sozeau	2014-09-27
*	Index keys instead of simply global references.	Matthieu Sozeau	2014-09-27
*	First version of keyed subterm selection in unification.	Matthieu Sozeau	2014-09-27
*	Fix test-suite file.	Matthieu Sozeau	2014-09-27
*	Fix bug #3664 by refolding projections that don't reduce in cbn.	Matthieu Sozeau	2014-09-27
*	Remove auto's use of dummy goal, use the proper sigma for pattern_of_constr.	Matthieu Sozeau	2014-09-27
*	Fix semantics of matching with folded/unfolded projections to definitely	Matthieu Sozeau	2014-09-27
*	Fix bug #3672, application of primitive projections as coercions.	Matthieu Sozeau	2014-09-27
*	Fix bug 3662 by actually reducing primitive projections in cbv/compute.	Matthieu Sozeau	2014-09-27
*	Bug fixed.	Matthieu Sozeau	2014-09-27
*	Make pattern_of_constr typed so that we can infer the proper patterns	Matthieu Sozeau	2014-09-27
*	Add a boolean to indicate the unfolding state of a primitive projection,	Matthieu Sozeau	2014-09-27
*	Adapting to naming of evars.	Hugo Herbelin	2014-09-27
*	Changed semantics of induction !id when a clause is given: don't	Hugo Herbelin	2014-09-27
*	Removing the last use of tclSENSITIVE in favour of tclNEWGOALS.	Pierre-Marie Pédrot	2014-09-27
*	Adding a tclNEWGOALS primitive.	Pierre-Marie Pédrot	2014-09-26
*	Hurkens.v: Fix a syntax error.	Arnaud Spiwack	2014-09-26
*	Fix canonical structure resolution which was launched on the results of	Matthieu Sozeau	2014-09-26
*	ClassicalFacts: adds a proof that weak excluded middle implies weak proof irr...	Arnaud Spiwack	2014-09-26
*	Hurkens.v: new paradox: type of modal propositions is not a retract.	Arnaud Spiwack	2014-09-26
*	Hurkens.v: fix coqdoc formatting in a comment.	Arnaud Spiwack	2014-09-26
*	Add a bunch of reproduction files for bugs.	Xavier Clerc	2014-09-26
*	Add missing "Fail" to bug cases.	Xavier Clerc	2014-09-26
*	Bug #3566 is fixed.	Xavier Clerc	2014-09-26
*	Adding a test for bug #3653.	Pierre-Marie Pédrot	2014-09-26
*	Test cases for closed bugs.	Xavier Clerc	2014-09-26
*	Fix incorrect assert false in detyping.	Matthieu Sozeau	2014-09-25
*	Revert changes of commit 4e1135fb315eab7 over file "plugins/micromega/sos.ml",	Xavier Clerc	2014-09-25
*	Add several reproduction files for bugs.	Xavier Clerc	2014-09-25
*	Improve consistency of whitespace (beautifier).	Xavier Clerc	2014-09-25
*	Remove some 'deprecated' warnings.	Xavier Clerc	2014-09-25
*	Hurkens.v: update comments.	Arnaud Spiwack	2014-09-25