coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[api] Misctypes removal: miscellaneous aliases.	Emilio Jesus Gallego Arias	2018-06-12
\|
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|
*	[ast] Improve precision of Ast location recognition in serialization.	Emilio Jesus Gallego Arias	2018-02-22
\| \| \| \| \| \| \| \| \|	We follow the suggestions in #402 and turn uses of `Loc.located` in `vernac` into `CAst.t`. The impact should be low as this change mostly affects top-level vernaculars. With this change, we are even closer to automatically map a text document to its AST in a programmatic way.
*	Moving Metasyntax.register_grammar to Pcoq for usability in Egramcoq.	Hugo Herbelin	2018-02-20
\| \| \| \|	Renaming it register_grammars_by_name.
*	Change references to CAMLP4 to CAMLP5 to be more accurate since we no	Jim Fehrle	2018-02-17
\| \| \| \|	longer use camlp4.
*	Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).	Hugo Herbelin	2017-10-05
\| \| \| \| \| \| \| \| \| \| \| \| \|	This allows e.g. the following to work: Reserved Notation "* a" (at level 70). Inductive P {n : nat} : nat -> Prop := c m : m where " m" := (P m). We seize this opportunity to make main calls to Metasyntax to depend on an arbitrary env rather than on Global.env. Incidentally, this fixes a little coqdoc bug in classifying the inductive type referred to in the "where" clause.
*	deprecate Pp.std_ppcmds type alias	Matej Košík	2017-07-27
\|
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	[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.