coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[api] Remove type equalities from API.	Emilio Jesus Gallego Arias	2017-07-25
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Add missing definition and fix #use include;; as suggested by @amintimany.	Théo Zimmermann	2017-06-22
*	Fix a bug in cumulativity	Amin Timany	2017-06-16
*	Clean up universes of constants and inductives	Amin Timany	2017-06-16
*	Squashed commit of the following:	Amin Timany	2017-06-16
*	Remove (useless) aliases from the API.	Matej Košík	2017-06-10
*	Put all plugins behind an "API".	Matej Kosik	2017-06-07
*	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\
\| *	Adding support for using grammar entries returning no value in EXTEND.	Hugo Herbelin	2017-05-16
\| *	Fix warnings in top_printers	Gaetan Gilbert	2017-05-08
\| *	Remove unused [open] statements	Gaetan Gilbert	2017-04-27
\| *	Locally disable some warnings.	Gaetan Gilbert	2017-04-27
* \|	[location] Remove `Loc.internal_ghost`	Emilio Jesus Gallego Arias	2017-04-25
* \|	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias	2017-04-25
* \|	[location] Switch glob_constr to Loc.located	Emilio Jesus Gallego Arias	2017-04-24
\|/
*	Merge branch 'trunk' into pr379	Maxime Dénès	2017-03-24
\|\
\| *	[pp] Make feedback the only logging mechanism.	Emilio Jesus Gallego Arias	2017-03-21
\| *	Fixing #use"include" after vernac is added and ltac is moved to a plugin.	Hugo Herbelin	2017-02-23
* \|	Merge branch 'master'.	Pierre-Marie Pédrot	2017-02-14
\|\\|
* \|	Moving printing code from Evd to Termops.	Pierre-Marie Pédrot	2017-02-14
* \|	Ltac now uses evar-based constrs.	Pierre-Marie Pédrot	2017-02-14
* \|	Tactic_matching API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| *	Adding a printer for Proof.proof reflecting the focusing layout.	Hugo Herbelin	2017-01-26
* \|	Introducing a new EConstr.t type to perform the nf_evar operation on demand.	Pierre-Marie Pédrot	2016-11-08
\|/
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-24
\|\
\| *	Remove no longer exported debug printer	Matthieu Sozeau	2016-10-21
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-08
\|\\|
\| *	Adding debugging printer for Genarg.ArgT.t.	Hugo Herbelin	2016-10-08
* \|	Merging Stdarg and Constrarg.	Pierre-Marie Pédrot	2016-09-21
\|/
*	Fixing extra returns in top_printers.ml (msg_notice not same semantics as pp).	Hugo Herbelin	2016-07-19
*	closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)	Pierre Letouzey	2016-07-03
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-01
\|\
* \|	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
\| *	Pfedit.get_current_context refinement (fix #4523)	Matthieu Sozeau	2016-05-26
* \|	Removing the Entry module now that rules need not be marshalled.	Pierre-Marie Pédrot	2016-05-10
* \|	Moving the Val module to Geninterp.	Pierre-Marie Pédrot	2016-05-04
* \|	Fixing printing of toplevel values.	Pierre-Marie Pédrot	2016-04-08
* \|	Do not export entry_key from Pcoq anymore.	Pierre-Marie Pédrot	2016-03-19
* \|	Simplifying the code of Entry.	Pierre-Marie Pédrot	2016-03-19
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Removing constr generic argument.	Pierre-Marie Pédrot	2016-01-14
* \|	Simplification of grammar_prod_item type.	Pierre-Marie Pédrot	2016-01-02
* \|	Finer-grained types for toplevel values.	Pierre-Marie Pédrot	2015-12-21
* \|	Using dynamic values in tactic evaluation.	Pierre-Marie Pédrot	2015-12-21
* \|	Tying the loop in tactic printing API.	Pierre-Marie Pédrot	2015-12-18
* \|	Type-safe Egramml.grammar_prod_item.	Pierre-Marie Pédrot	2015-10-27
* \|	Pcoq entries are given a proper module.	Pierre-Marie Pédrot	2015-10-26