coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-29
\|\\|
\| *	Restore warnings produced by the interpretation of the command line	Hugo Herbelin	2016-01-22
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
* \|	Stronger invariants on the use of the introduction pattern (pat1,...,patn).	Hugo Herbelin	2016-01-21
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Moving val_cast to Tacinterp.	Pierre-Marie Pédrot	2016-01-17
* \|	Getting rid of the awkward unpack mechanism from Genarg.	Pierre-Marie Pédrot	2016-01-17
* \|	Simplification and type-safety of Pcoq thanks to GADTs in Genarg.	Pierre-Marie Pédrot	2016-01-17
* \|	Exporting Genarg implementation in the API.	Pierre-Marie Pédrot	2016-01-17
* \|	Reimplementing Genarg safely.	Pierre-Marie Pédrot	2016-01-17
* \|	Adding a structure indexed by tags.	Pierre-Marie Pédrot	2016-01-17
* \|	Temporary commit getting rid of Obj.magic unsafety for Genarg.	Pierre-Marie Pédrot	2016-01-17
\| *	Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.	Maxime Dénès	2016-01-15
* \|	Removing constr generic argument.	Pierre-Marie Pédrot	2016-01-14
* \|	Removing ident and var generic arguments.	Pierre-Marie Pédrot	2016-01-14
* \|	Merge remote-tracking branch 'origin/v8.5' into trunk	Guillaume Melquiond	2016-01-06
\|\\|
\| *	Protect code against changes in Map interface.	Maxime Dénès	2016-01-06
\| *	Fix order of files in mllib.	Maxime Dénès	2016-01-05
\| *	COMMENTS: Predicate	Matej Kosik	2016-01-05
* \|	Remove some unused functions.	Guillaume Melquiond	2016-01-02
* \|	Remove some useless module opening.	Guillaume Melquiond	2016-01-02
* \|	Avoid warnings about loop indices.	Guillaume Melquiond	2016-01-02
* \|	Fix typos.	Guillaume Melquiond	2016-01-01
* \|	Remove unused hashconsing code.	Guillaume Melquiond	2016-01-01
* \|	Do not make it harder on the compiler optimizer by packing arguments.	Guillaume Melquiond	2016-01-01
* \|	Merge branch 'v8.5' into trunk	Guillaume Melquiond	2015-12-31
\|\\|
* \|	Do not compose List.length with List.filter.	Guillaume Melquiond	2015-12-31
\| *	Do not dump a glob reference when its location is ghost. (Fix bug #4469)	Guillaume Melquiond	2015-12-31
* \|	Removing the special status of open_constr generic argument.	Pierre-Marie Pédrot	2015-12-28
* \|	Finer-grained types for toplevel values.	Pierre-Marie Pédrot	2015-12-21
* \|	Removing ad-hoc interpretation rules for tactic notations and their genarg.	Pierre-Marie Pédrot	2015-12-21
* \|	Sharing toplevel representation for several generic types.	Pierre-Marie Pédrot	2015-12-21
* \|	Removing the now useless genarg generic argument.	Pierre-Marie Pédrot	2015-12-21
* \|	Using dynamic values in tactic evaluation.	Pierre-Marie Pédrot	2015-12-21
* \|	Attaching a dynamic argument to the toplevel type of generic arguments.	Pierre-Marie Pédrot	2015-12-21
* \|	Trust the directory cache in batch mode.	Guillaume Melquiond	2015-12-21
* \|	COMMENTS: added to the "Unicode" module.	Matej Kosik	2015-12-18
* \|	COMMENTS: updated in the "Option" module.	Matej Kosik	2015-12-18
* \|	COMMENTS: added to the "Predicate" module	Matej Kosik	2015-12-18
\| *	spawn: fix leak of file descriptors	Enrico Tassi	2015-12-17
* \|	Getting rid of some hardwired generic arguments.	Pierre-Marie Pédrot	2015-12-17
* \|	Adding compatibility flag for 8.5.	Hugo Herbelin	2015-12-14
* \|	Remove some occurrences of Unix.opendir.	Guillaume Melquiond	2015-12-14
* \|	Removing dead unsafe code in Genarg.	Pierre-Marie Pédrot	2015-12-12
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-11
\|\\|
\| *	Fixing compilation with OCaml 3.12 after commit 9d45d45f3a87 on removing	Hugo Herbelin	2015-12-10
\| *	Remove remaining occurrences of Unix.readdir.	Guillaume Melquiond	2015-12-09
\| *	Replace Unix.readdir by Sys.readdir in dir cache.	Emilio Jesus Gallego Arias	2015-12-09
* \|	Factorizing unsafe code by relying on the new Dyn module.	Pierre-Marie Pédrot	2015-12-05
* \|	Leveraging GADTs to provide a better Dyn API.	Pierre-Marie Pédrot	2015-12-05