coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Fixing the return type of the Atoken symbol.	Pierre-Marie Pédrot	2015-10-28
\|
*	Removing unused code in Pcoq.	Pierre-Marie Pédrot	2015-10-27
\|
*	Finer type for Pcoq.interp_entry_name.	Pierre-Marie Pédrot	2015-10-27
\|
*	Indexing existentially quantified entries returned by interp_entry_name.	Pierre-Marie Pédrot	2015-10-27
\|
*	Type-safe grammar extensions.	Pierre-Marie Pédrot	2015-10-27
\|
*	Pcoq entries are given a proper module.	Pierre-Marie Pédrot	2015-10-26
\| \| \| \| \| \| \| \| \| \| \|	Entries defined in the Pcoq AST of symbols must be marshallable, because they are present in the libstack. Yet, CAMLP4/5 entries are not marshallable as they contain functional values. This is why the Pcoq module used a pair [string * string] to describe entries. It is obviously type-unsafe, so we define a new abstract type in its own module. There is a little issue though, which is that our entries and CAMLP4/5 entries must be kept synchronized through an association table. The Pcoq module tries to maintain this invariant.
*	Getting rid of the Atactic entry.	Pierre-Marie Pédrot	2015-10-25
\|
*	Getting rid of the Agram entry.	Pierre-Marie Pédrot	2015-10-25
\|
*	Pcoq.prod_entry_key now uses a GADT to statically enforce typedness.	Pierre-Marie Pédrot	2015-10-21
\|
*	Turn Pcoq into a regular ML file.	Pierre-Marie Pédrot	2015-10-21