coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Notation: option to attach extra pretty printing rules to notations	Enrico Tassi	2014-09-29
*	Additional entry tactic_arg in Print Grammar tactic.	Pierre-Marie Pédrot	2014-09-03
*	Getting rid of atomic tactics in Tacenv.	Pierre-Marie Pédrot	2014-08-31
*	Moving the TacExtend node from atomic to plain tactics.	Pierre-Marie Pédrot	2014-08-18
*	Qualified ML tactic names. The plugin name is used to discriminate	Pierre-Marie Pédrot	2014-07-27
*	Useless keeping of dirpath in tactic aliases.	Pierre-Marie Pédrot	2014-06-30
*	Fix the behaviour of ML tactic notations w.r.t. Imports by making them	Pierre-Marie Pédrot	2014-05-13
*	Now parsing rules of ML-declared tactics are only made available after the	Pierre-Marie Pédrot	2014-05-12
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Remove some dead-code (thanks to ocaml warnings)	Pierre Letouzey	2014-03-05
*	Useless check when loading notations through import.	Pierre-Marie Pédrot	2014-03-01
*	Fixing printing of only_parsing notations.	Pierre-Marie Pédrot	2014-02-25
*	Notations can now accept dummy arguments. If ever a bound variable is not	Pierre-Marie Pédrot	2013-12-22
*	Removing the dependency of every level of tactic ATSs on glob_tactic_expr.	ppedrot	2013-11-10
*	Revert the previous commit. It broke Coq compilation.	ppedrot	2013-11-09
*	Removing the dependency of every level of tactic ATSs on glob_tactic_expr.	ppedrot	2013-11-09
*	Moving notation types into grammar rule.	ppedrot	2013-11-09
*	Cleaning and documenting Egramcoq.	ppedrot	2013-11-09
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	cList.index is now cList.index_f, same for index0	letouzey	2013-10-23
*	cList: set-as-list functions are now with an explicit comparison	letouzey	2013-10-23
*	enhance marshallable option for freeze (minor TODO in safe_typing)	gareuselesinge	2013-08-08
*	Replacing uses of association lists by maps in notations.	ppedrot	2013-08-03
*	More dynamic argument scopes	letouzey	2013-07-17
*	States: frozen states can hold closures	gareuselesinge	2013-05-06
*	Avoid a few overzealous "when Errors.noncritical"	letouzey	2013-03-17
*	Restrict (try...with...) to avoid catching critical exn (part 13)	letouzey	2013-03-13
*	More monomorphization.	ppedrot	2013-03-05
*	Actually adding backtrace handling.	ppedrot	2013-01-28
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	Fixed bug #2967 (some missing check on ill-formed recursive notation strings).	herbelin	2013-01-27
*	Modulification of identifier	ppedrot	2012-12-14
*	Using library string functions.	ppedrot	2012-12-13
*	Renamed Option.Misc.compare to the more uniform Option.equal.	ppedrot	2012-12-13
*	Revised the strategy for automatic insertion of spaces when printing	herbelin	2012-12-04
*	Monomorphization (toplevel)	ppedrot	2012-11-26
*	Taking into account the type of a definition (if it exists), and the	herbelin	2012-11-17
*	Added a CString module.	ppedrot	2012-11-13
*	Monomorphized a lot of equalities over OCaml integers, thanks to	ppedrot	2012-11-08
*	Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp	letouzey	2012-10-16
*	still some more dead code removal	letouzey	2012-10-06
*	Adding a nominal typing layer to Metasyntax in order to clarify	ppedrot	2012-10-04
*	Moved Compat to parsing. This permits to break the dependency of the	ppedrot	2012-10-04
*	Cleaning interface of Util.	ppedrot	2012-09-18
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	The new ocaml compiler (4.00) has a lot of very cool warnings,	regisgia	2012-09-14
*	Added support for option Local (at module level) in Tactic Notation.	herbelin	2012-08-11
*	Updating headers.	herbelin	2012-08-08
*	Notation: a new annotation "compat 8.x" extending "only parsing"	letouzey	2012-07-05