coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| \| \| \| * \| \| \| \| \| \|	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#518: Faster universe unification	Maxime Dénès	2017-05-23
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	[vernac] Remove `Save thm id.` command.	Emilio Jesus Gallego Arias	2017-05-23
\| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	[vernac] Remove `Save.` command.	Emilio Jesus Gallego Arias	2017-05-23
\| \|_\|_\|_\|_\|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| * \|	refl_omega: some code refactoring	Pierre Letouzey	2017-05-22
\| \| \| \| \| \| \| \| \| \| \| \| \| * \|	refl_omega.v: explicitely identify atom indexes and omega vars	Pierre Letouzey	2017-05-22
\| \| \| \| \| \| \| \| \| \| \| \| \| * \|	ReflOmegaCore: misc cleanup, <? instead of bgt, etc	Pierre Letouzey	2017-05-22
\| \| \| \| \| \| \| \| \| \| \| \| \| * \|	ROmega : O_STATE turned into a O_SUM	Pierre Letouzey	2017-05-22
\| \| \| \| \| \| \| \| \| \| \| \| \| * \|	ROmega: less contructors in the final omega trace	Pierre Letouzey	2017-05-22
\| \| \| \| \| \| \| \| \| \| \| \| \| * \|	ROmega : merge O_CONSTANT* into a single O_BAD_CONSTANT	Pierre Letouzey	2017-05-22
\| \| \| \| \| \| \| \| \| \| \| \| \| * \|	ReflOmegaCore: reverse some integer mult (coefs k1,k2 will often be simple)	Pierre Letouzey	2017-05-22
\| \| \| \| \| \| \| \| \| \| \| \| \| * \|	ReflOmegaCore: comment, reorganize, permut some constructors, etc	Pierre Letouzey	2017-05-22
\| \| \| \| \| \| \| \| \| \| \| \| \| * \|	romega: add a tactic named unsafe_romega (for debugging, or bold users)	Pierre Letouzey	2017-05-22
\| \| \| \| \| \| \| \| \| \| \| \| \| * \|	romega: no more normalization trace, replaced by some Coq-side computation	Pierre Letouzey	2017-05-22
\| \| \| \| \| \| \| \| \| \| \| \| \| * \|	romega/const_omega : a few improvements (less try with, no gen equality)	Pierre Letouzey	2017-05-22
\| \| \| \| \| \| \| \| \| \| \| \| \| * \|	romega: use N instead of nat for Tvar	Pierre Letouzey	2017-05-22
\| \| \| \| \| \| \| \| \| \| \| \| \| * \|	romega: shorter trace (no more term lengths)	Pierre Letouzey	2017-05-22
\| \| \| \| \| \| \| \| \| \| \| \| \| * \|	refl_omega: refactoring of normalize_equation	Pierre Letouzey	2017-05-22
\| \| \| \| \| \| \| \| \| \| \| \| \| * \|	ReflOmegaCore: lots of dead code + a few refactored proofs	Pierre Letouzey	2017-05-22
\| \| \| \| \| \| \| \| \| \| \| \| \| * \|	romega: if it bugs again, at least do it with a short and quick error	Pierre Letouzey	2017-05-22
\| \| \| \| \| \| \| \| \| \| \| \| \| * \|	refl_omega: comment the lack of lifts when dealing with arrows	Pierre Letouzey	2017-05-22
\| \| \| \| \| \| \| \| \| \| \| \| \| * \|	romega: discard constructor D_mono (shorter trace + fix a bug)	Pierre Letouzey	2017-05-22
\| \| \| \| \| \| \| \| \| \| \| \| \| * \|	refl_omega: more refactoring (e.g. IntSets instead of sorted lists)	Pierre Letouzey	2017-05-22
\| \| \| \| \| \| \| \| \| \| \| \| \| * \|	refl_omega: refactoring (e.g. useless args in destructurate_pos_hyp)	Pierre Letouzey	2017-05-22
\| \| \| \| \| \| \| \| \| \| \| \| \| * \|	ReflOmegaCore: discard useless cosntructor P_NOP	Pierre Letouzey	2017-05-22