coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Revert "KEYID token makes parsing more robust in face of notations"	gareuselesinge	2013-06-21
*	Revert "parse "of" as KEYID "of""	gareuselesinge	2013-06-21
*	parse "of" as KEYID "of"	gareuselesinge	2013-06-19
*	KEYID token makes parsing more robust in face of notations	gareuselesinge	2013-06-19
*	Proof-of-concept: moved four easy-to-handle generic arguments to	ppedrot	2013-06-18
*	More comments in Genarg.	ppedrot	2013-06-06
*	Uniformizing generic argument types.	ppedrot	2013-06-06
*	Setting "appcontext" as the default behaviour in Ltac matching.	ppedrot	2013-05-28
*	Fixing warning of deprecated Argument Scopes.	ppedrot	2013-05-28
*	Use the Hook module here and there.	ppedrot	2013-05-12
*	States: frozen states can hold closures	gareuselesinge	2013-05-06
*	Egramcoq+Lexer : no need for an init_function	letouzey	2013-04-23
*	Egramcoq: clean an ugly code snippet	letouzey	2013-04-23
*	code simplifications concerning Summary	letouzey	2013-04-22
*	Renaming SearchAbout into Search and Search into SearchHead.	herbelin	2013-04-17
*	More functional implementation of locality_flag and program_mode	gareuselesinge	2013-04-15
*	cbn can be called by Eval	pboutill	2013-03-25
*	Pptactic.pr_raw_tactic is now without env argument	letouzey	2013-03-14
*	Modules and ppvernac, sequel of Enrico's commit 16261	letouzey	2013-03-13
*	Restrict (try...with...) to avoid catching critical exn (part 9)	letouzey	2013-03-13
*	Restrict (try...with...) to avoid catching critical exn (part 8)	letouzey	2013-03-13
*	Allowing (Co)Fixpoint to be defined local and Let-style.	ppedrot	2013-03-11
*	Added a Local Definition vernacular command. This type of definition	ppedrot	2013-03-11
*	avoid (Int.equal (cmp ...) 0) when a boolean equality exists	letouzey	2013-02-19
*	Dir_path --> DirPath	letouzey	2013-02-19
*	Removing Exc_located and using the new exception enrichement	ppedrot	2013-02-18
*	use List.rev_map whenever possible	letouzey	2013-02-18
*	Useless use of hooks in VernacDefinition. In addition, this was	ppedrot	2013-02-10
*	Actually adding backtrace handling.	ppedrot	2013-01-28
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	New implementation of the conversion test, using normalization by evaluation to	mdenes	2013-01-22
*	Avoiding collision between Camlp4 Loc.Exc_located and Coq's Loc.Exc_located.	herbelin	2012-12-22
*	Yet a new reduction tactic in Coq : cbn	pboutill	2012-12-21
*	Modulification of name	ppedrot	2012-12-18
*	Modulification of dir_path	ppedrot	2012-12-14
*	Modulification of identifier	ppedrot	2012-12-14
*	Early translation of camlp4/camlp5 located errors into coq-located	herbelin	2012-12-04
*	Monomorphization (parsing)	ppedrot	2012-11-25
*	backtrack too much commited files in the last commit.	courtieu	2012-11-15
*	Fixing emacs diff bug with .dir-locals.el.	courtieu	2012-11-15
*	More monomorphizations	ppedrot	2012-11-13
*	Monomorphized a lot of equalities over OCaml integers, thanks to	ppedrot	2012-11-08
*	Fix reference_or_constr grammar rule to accept @t as a constr	gareuselesinge	2012-11-07
*	Change [Hints Resolve] to still accept constrs as arguments	msozeau	2012-10-31
*	Fixed #2926:	ppedrot	2012-10-29
*	Change Hint Resolve, Immediate to take a global reference as argument	msozeau	2012-10-26
*	Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp	letouzey	2012-10-16
*	Egramml: minor simplification	letouzey	2012-10-15
*	restore compatibility with camlp5 < 6.00	letouzey	2012-10-06
*	still some more dead code removal	letouzey	2012-10-06