coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
\| \| \| \| * \| \|	[checker] [votour] resolve warning 52 fragile constant pattern	Gaëtan Gilbert	2017-05-26
\| \| \| \|/ / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Also stop using failwith for flow control in tuple_of_string.
* \| \| \| \| \|	Merge PR#666: romega revisited : no more normalization trace, cleaned-up ↵	Maxime Dénès	2017-05-26
\|\ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	resolution trace
* \ \ \ \ \ \	Merge PR#655: Extra functions exported in EConstr	Maxime Dénès	2017-05-26
\|\ \ \ \ \ \ \ \| \|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \|
\| \| \| \| \| * \|	[checker] Add bin/votour to the coqocaml target.	Emilio Jesus Gallego Arias	2017-05-26
\| \| \| \| \| \| \|
\| \| \| \| \| * \|	[votour] Fix/disable warnings.	Emilio Jesus Gallego Arias	2017-05-26
\| \| \| \| \| \| \|
\| \| \| \| \| * \|	[votour] Fix build with -safe-string (bug 5553)	Emilio Jesus Gallego Arias	2017-05-26
\| \|_\|_\|_\|/ / \|/\| \| \| \| \|
\| \| \| \| * \|	add Show test with -emacs flag	Paul Steckler	2017-05-25
\| \|_\|_\|/ / \|/\| \| \| \|
* \| \| \| \|	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The trace only mentions the constant k by which we want to divide the equation, not anymore the equation we obtain after the division. Shorter trace, and it won't take much more time to perform the few Z.div than checking as currently the equality of the initial equation and the final equation multiplied by k.
\| \| \| * \| \| \| \| \| \| \|	[option] Remove support for non-synchronous options.	Emilio Jesus Gallego Arias	2017-05-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which this PR solves, I propose to remove support for non-synchronous options. It seems the few uses of `optsync = false` we legacy and shouldn't have any impact. Moreover, non synchronous options may create particularly tricky situations as for instance, they won't be propagated to workers.
\| \| * \| \| \| \| \| \| \| \|	coq_makefile: use -include rather than include	Enrico Tassi	2017-05-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This fixes bedrock and eliminates warnings. Thanks Jason Gross for debugging this!
* \| \| \| \| \| \| \| \| \| \|	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This makes the following work correctly: make only TGTS="foo bar" -j2 note that make foo bar -j2 is not doing what you think
\| \| \| \| * \| \| \| \| \| \| \|	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Restores compatibility with 8.6
\| \| \| \| * \| \| \| \| \| \| \|	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Used to guess again the ocamlfind location at Coq's execution time. An option to override the value (inferred at ./configure time) is available. So, what is the point of guessing it? Either it stays there, or the user is doing a hack, and has a flag to do it.
\| \| \| \| * \| \| \| \| \| \| \|	coqdep: set FOR_PACK variable for files that need to be packed	Enrico Tassi	2017-05-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This enables one to have just one rule to compile .ml -> .cmx. By using $(FOR_PACK) in such rule one passes to ocamlopt -for-pack ModName only when necessary. Before this coq_makefile had to generate 2 different rules, depending if the module was mentioned in an .mlpack.
\| \| \| \| * \| \| \| \| \| \| \|	print_config: print COQ_SRC_SUBDIRS	Enrico Tassi	2017-05-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This way a makefile can just iterate on this list, intead of having a bunch of -I hardcoded in there by coq_makefile
\| \| \| \| * \| \| \| \| \| \| \|	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	and avoid duplication
\| \| \| \| * \| \| \| \| \| \| \|	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The .mli only acknowledges the current API. I'm not guilty your honor!
\| \| \| \| * \| \| \| \| \| \| \|	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 ↵	Maxime Dénès	2017-05-23
\|\ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	with binders)
* \ \ \ \ \ \ \ \ \ \ \	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \