coq - The formal proof system

Age	Commit message (Collapse)	Author
2017-03-14	Merge PR#412: Remove outdated comment from 2002.	Maxime Dénès

2017-03-14	[future] Remove unused parameter greedy.	Emilio Jesus Gallego Arias
	It was always set to `greedy:true`.
2017-02-22	Merge branch 'v8.6'	Pierre-Marie Pédrot

2017-02-20	Merge PR#189: Remove tabulation support from pretty-printing.	Maxime Dénès

2017-02-15	Make Obligations see fix_exn	Enrico Tassi

2017-02-15	[stm] Reenable Show Script command.	Emilio Jesus Gallego Arias
	We extend `Stm.vernac_interp` so it can handle the commands it should by level. This reenables `Show Script` handling, and this interpretation function should handle more commands in the future such as Load. However note that we must first refactor the parsing state handling a bit and remove the legacy `Stm.interp` before that.
2017-02-15	[stm] Break stm/toplevel dependency loop.	Emilio Jesus Gallego Arias
	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.