coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| \| * \| \| \|	minor clarifications in constrintern.ml:sort_fields	Gabriel Scherer	2016-06-27
\| \|/ / / / \|/\| \| \| \|
\| * \| \| \|	Patterns in binders: printing tests	Arnaud Spiwack	2016-06-27
\| * \| \| \|	Patterns in binders: functional tests	Arnaud Spiwack	2016-06-27
\|/ / / /
* \| \| \|	Merge branch 'funpattern' into trunk. Was PR#142: Binder syntax.	Maxime Dénès	2016-06-27
\|\ \ \ \
\| * \| \| \|	Adding ability to put any pattern in binders, prefixed by a quote.	Daniel de Rauglaudre	2016-06-27
\| \| \| * \|	More on f9695eb4b, 827663982 on resolving #4782, #4813 (typing "with" clause).	Hugo Herbelin	2016-06-27
\| \| \| * \|	Fix bug #4698: CoqIDE error dialogs piling up when coqtop dies.	Pierre-Marie Pédrot	2016-06-27
\| \| * \| \|	[xmlproto] Remove duplicated deserialization.	Emilio Jesus Gallego Arias	2016-06-25
\| \| * \| \|	[doc] Update changes for feedback.	Emilio Jesus Gallego Arias	2016-06-25
\| \| * \| \|	[feedback] Remove `ErrorMsg` in favor of `Message Error`.	Emilio Jesus Gallego Arias	2016-06-25
\| \| * \| \|	[feedback] Allow messages to carry a location.	Emilio Jesus Gallego Arias	2016-06-25
\| \| * \| \|	[feedback] Add optional ?loc parameter to loggers.	Emilio Jesus Gallego Arias	2016-06-25
\| \| * \| \|	[feedback] Remove unused tag on `Debug` level.	Emilio Jesus Gallego Arias	2016-06-25
\| \| * \| \|	[merlin] Fix .merlin STM includes.	Emilio Jesus Gallego Arias	2016-06-25
\| \|/ / /
* \| \| \|	Several easy but efficient optimizations for subst and clear tactics.	Pierre-Marie Pédrot	2016-06-24
\|\\| \| \|
\| * \| \|	Optimize the subst tactic.	Pierre-Marie Pédrot	2016-06-24
\| * \| \|	Optmimize the subst tactic.	Pierre-Marie Pédrot	2016-06-24
\| * \| \|	Optim in Clenv: use noccurn instead of depends.	Pierre-Marie Pédrot	2016-06-24
\| * \| \|	Optimize the subst tactic.	Pierre-Marie Pédrot	2016-06-24
\| * \| \|	Optimize the clear tactic.	Pierre-Marie Pédrot	2016-06-24
\| * \| \|	Optimize the clear tactic.	Pierre-Marie Pédrot	2016-06-24
\| * \| \|	Optimization in the subst tactic.	Pierre-Marie Pédrot	2016-06-24
\| * \| \|	Optimization in the subst tactic.	Pierre-Marie Pédrot	2016-06-24
\| * \| \|	Optimization in the subst tactic.	Pierre-Marie Pédrot	2016-06-24
\|/ / /
* \| \|	Removing tactic compatibility layers in setoid_ring.	Pierre-Marie Pédrot	2016-06-24
* \| \|	Fixing #4854 (regression introduced in 4d25b224 in relation with #4592).	Hugo Herbelin	2016-06-24
* \| \|	Makefile.install: fix a typo in last commit c954bb5, sorry	Pierre Letouzey	2016-06-24
* \| \|	remove an old workaround for OCaml 3.11 + MacOS natdynlink	Pierre Letouzey	2016-06-24
* \| \|	Makefile.build: mitigate potential issues with multiple creations of pack .cmi	Pierre Letouzey	2016-06-24
* \| \|	Makefile.install: fix the install of plugin cmi	Pierre Letouzey	2016-06-24
* \| \|	Better algorithm for variable deambiguation in term printing.	Pierre-Marie Pédrot	2016-06-23
* \| \|	Makefile.doc: fix 'make doc'	Pierre Letouzey	2016-06-23
\| * \|	Fix typo.	Guillaume Melquiond	2016-06-23
\| * \|	Remove extraction-specific code from the checker.	Guillaume Melquiond	2016-06-23
* \| \|	Makefile.build: "make;make" should redo nothing	Pierre Letouzey	2016-06-22
* \| \|	Makefile: compat5* moved in grammar/, less -I given to camlp4o	Pierre Letouzey	2016-06-21
* \| \|	Parsing/compat.ml4: avoid "let open" syntax, unsupported by my camlp5 6.11	Pierre Letouzey	2016-06-21
* \| \|	Merge remote-tracking branch 'github/pr/212' into trunk	Maxime Dénès	2016-06-20
\|\ \ \
\| \| * \|	Reference Manual / Extraction: the original example command no longer works w...	Matej Kosik	2016-06-20
\| * \| \|	Add file name, line number and beginning of line position to locations.	Maxime Dénès	2016-06-20
* \| \| \|	LtacProf reports structured results (pr/209)	CJ Bell	2016-06-20
* \| \| \|	COMMENTS: Vernacexpr.extend_name	Matej Kosik	2016-06-20
* \| \| \|	Small optimization in clear_body.	Pierre-Marie Pédrot	2016-06-20
* \| \| \|	Fix bug #4825: [clear] should not dependency-check hypotheses that come above...	Pierre-Marie Pédrot	2016-06-20
* \| \| \|	Prevent a useless evar normalization in Clenvtac.unify.	Pierre-Marie Pédrot	2016-06-20
* \| \| \|	Do not evar-normalize goals when interpreting some hardwired genargs.	Pierre-Marie Pédrot	2016-06-20
\| \| \| *	Add [Unset Printing Dependent Evars Line]	Jason Gross	2016-06-19
\| \|_\|/ \|/\| \|
* \| \|	Merge 'pr/215' into trunk	Enrico Tassi	2016-06-19
\|\ \ \
* \| \| \|	Fix bug #4836: Anomaly: Uncaught exception Invalid_argument.	Pierre-Marie Pédrot	2016-06-19
\| * \| \|	Fix path separator on windows	Jason Gross	2016-06-18