coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[coqlib] Deprecate redundant Coqlib functions.	Emilio Jesus Gallego Arias	2017-05-27
*	Merge PR#686: [travis] temporary UniMath overlay	Maxime Dénès	2017-05-27
\|\
\| *	[travis] temporary UniMath overlay	Maxime Dénès	2017-05-27
\|/
*	Merge PR#666: romega revisited : no more normalization trace, cleaned-up reso...	Maxime Dénès	2017-05-26
\|\
* \	Merge PR#655: Extra functions exported in EConstr	Maxime Dénès	2017-05-26
\|\ \
* \ \	Merge PR#645: [stm] Tweak debug options.	Maxime Dénès	2017-05-25
\|\ \ \
* \ \ \	Merge PR#637: Short cleaning of the interpretation path for constr_with_bindings	Maxime Dénès	2017-05-25
\|\ \ \ \
* \ \ \ \	Merge PR#608: Allow Ltac2 as a plugin	Maxime Dénès	2017-05-25
\|\ \ \ \ \
* \ \ \ \ \	Merge PR#481: [option] Remove support for non-synchronous options.	Maxime Dénès	2017-05-25
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR#406: coq makefile2	Maxime Dénès	2017-05-25
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR#402: Uniform attribute handling in interfaces	Maxime Dénès	2017-05-25
\|\ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \|	[location] [travis] Add overlays for located_switch	Emilio Jesus Gallego Arias	2017-05-25
\| * \| \| \| \| \| \| \|	[location] Fix warnings.	Emilio Jesus Gallego Arias	2017-05-24
\| * \| \| \| \| \| \| \|	[location] Renaming "CAst.ast" to "CAst.t"	Matej Košík	2017-05-24
\| * \| \| \| \| \| \| \|	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\| \|\ \ \ \ \ \ \ \ \| \|/ / / / / / / / \|/\| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| *	ROmega: division-aware ReflOmegaCore, allowing trace without terms	Pierre Letouzey	2017-05-24
\| \| \| * \| \| \| \| \|	[option] Remove support for non-synchronous options.	Emilio Jesus Gallego Arias	2017-05-24
\| \| * \| \| \| \| \| \|	coq_makefile: use -include rather than include	Enrico Tassi	2017-05-24
* \| \| \| \| \| \| \| \|	Merge PR#642: Small cleanup on `close_proof` type.	Maxime Dénès	2017-05-24
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR#650: Fixing an extra bug with pattern_of_constr	Maxime Dénès	2017-05-24
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR#671: unification.mli: Fix a spelling typo in a comment	Maxime Dénès	2017-05-24
\|\ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \|	unification.mli: Fix a spelling typo in a comment	Jason Gross	2017-05-23
\|/ / / / / / / / / /
\| \| \| \| * \| \| \| \| \|	add the only target	Enrico Tassi	2017-05-23
\| \| \| \| * \| \| \| \| \|	travis: coq_makefile needs the tipa package	Enrico Tassi	2017-05-23
\| \| \| \| * \| \| \| \| \|	overlay for UniMath	Enrico Tassi	2017-05-23
\| \| \| \| * \| \| \| \| \|	coq_makefile: avoid spurious ./ in generated .conf file	Enrico Tassi	2017-05-23
\| \| \| \| * \| \| \| \| \|	Restore 8.5, 8.6 compatibility of STDTIME, TIMECMD	Jason Gross	2017-05-23
\| \| \| \| * \| \| \| \| \|	coq_makefile: don't quote extra arguments (-arg)	Enrico Tassi	2017-05-23
\| \| \| \| * \| \| \| \| \|	Make install a single colon target for retro compatibility	Enrico Tassi	2017-05-23
\| \| \| \| * \| \| \| \| \|	enters coq_makefile2	Enrico Tassi	2017-05-23
\| \| \| \| * \| \| \| \| \|	test suite for coq_makefile2	Enrico Tassi	2017-05-23
\| \| \| \| * \| \| \| \| \|	coqdep: remove optimization making makefiles harder to write	Enrico Tassi	2017-05-23
\| \| \| \| * \| \| \| \| \|	ocamlfind: coqtop -config prints ocamlfind as found by ./configure	Enrico Tassi	2017-05-23
\| \| \| \| * \| \| \| \| \|	coqdep: set FOR_PACK variable for files that need to be packed	Enrico Tassi	2017-05-23
\| \| \| \| * \| \| \| \| \|	print_config: print COQ_SRC_SUBDIRS	Enrico Tassi	2017-05-23
\| \| \| \| * \| \| \| \| \|	Document --print-version in Usage	Enrico Tassi	2017-05-23
\| \| \| \| * \| \| \| \| \|	Put the list of Coq sources subdirectories in one place	Enrico Tassi	2017-05-23
\| \| \| \| * \| \| \| \| \|	Usage.print_config moved to Envars	Enrico Tassi	2017-05-23
\| \| \| \| * \| \| \| \| \|	CoqProject_file: document in API deprecated features	Enrico Tassi	2017-05-23
\| \| \| \| * \| \| \| \| \|	CoqProject_file: API and code cleanup (tuples -> records)	Enrico Tassi	2017-05-23
\| \| \| \| * \| \| \| \| \|	ide/project_file.ml4 -> lib/coqProject_file.ml4 + .mli	Enrico Tassi	2017-05-23
\| \| \| \| * \| \| \| \| \|	ide/project_fie.ml4: include standard banner with copyright	Enrico Tassi	2017-05-23
\| \| \| \| * \| \| \| \| \|	test suite for coq_makefile	Enrico Tassi	2017-05-23
\| \| \| \| * \| \| \| \| \|	configure: -local set coqdoc destination dir to ./doc rather than ""	Enrico Tassi	2017-05-23
\| \|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| *	Bigint.euclid: clarify which sign convention is used	Pierre Letouzey	2017-05-23
* \| \| \| \| \| \| \| \|	Merge PR#661: Added a test for #4765 (an example of printing abbreviation wit...	Maxime Dénès	2017-05-23
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR#659: Mention ./configure in INSTALL.doc	Maxime Dénès	2017-05-23
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR#657: [test-suite] Add tests for goal printing.	Maxime Dénès	2017-05-23
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR#646: Revised behavior on ill-formed identifiers	Maxime Dénès	2017-05-23
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#660: Change wrong bullet message.	Maxime Dénès	2017-05-23
\|\ \ \ \ \ \ \ \ \ \ \ \ \