coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[coqlib] Deprecate redundant Coqlib functions.	Emilio Jesus Gallego Arias	2017-05-27
\| \| \| \| \| \| \| \| \| \| \| \|	We remove redundant functions `coq_constant`, `gen_reference`, and `gen_constant`. This is a first step towards a lazy binding of libraries references. We have also chosen to untangle `constr` from `Coqlib`, as how to instantiate the reference (in particular wrt universes) is a client-side issue. (The client may want to provide an `evar_map` ?) c.f. #186
*	Merge PR#481: [option] Remove support for non-synchronous options.	Maxime Dénès	2017-05-25
\|\
* \	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\ \
\| \| *	[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.
\| *	Merge PR#627: Obligations shrinking: shrink abstraction too	Maxime Dénès	2017-05-20
\| \|\
\| * \|	Uniformity of style for selecting plural or not; spacing for comma.	Hugo Herbelin	2017-05-13
\| \| \|
\| \| *	Obligations shrinking: shrink abstraction too	Matthieu Sozeau	2017-05-11
\| \|/
\| *	More consistent writing of de Bruijn.	Théo Zimmermann	2017-05-01
\| \|
* \|	[location] Make location optional in Loc.located	Emilio Jesus Gallego Arias	2017-04-25
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This completes the Loc.ghost removal, the idea is to gear the API towards optional, but uniform, location handling. We don't print <unknown> anymore in the case there is no location. This is what the test suite expects. The old printing logic for located items was a bit inconsistent as it sometimes printed <unknown> and other times it printed nothing as the caller checked for `is_ghost` upstream.
* \|	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias	2017-04-25
\|/ \| \| \|	Now it is a private field, locations are optional.
*	Merge branch 'trunk' into pr379	Maxime Dénès	2017-03-24
\|
*	Make Obligations see fix_exn	Enrico Tassi	2017-02-15
\|
*	[stm] Break stm/toplevel dependency loop.	Emilio Jesus Gallego Arias	2017-02-15
	Currently, the STM, vernac interpretation, and the toplevel are intertwined in a mutual dependency that needs to be resolved using imperative callbacks. This is problematic for a few reasons, in particular it makes the interpretation of commands that affect the document quite intricate. As a first step, we split the `toplevel/` directory into two: "pure" vernac interpretation is moved to the `vernac/` directory, on which the STM relies. Test suite passes, and only one command seems to be disabled with this approach, "Show Script" which is to my understanding obsolete. Subsequent commits will fix this and refine some of the invariants that are not needed anymore.