coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Evarutil.(e_)new_Type: remove unused env argument	Gaëtan Gilbert	2018-07-03
*	Remove reference name type.	Maxime Dénès	2018-06-18
*	[api] Misctypes removal: several moves:	Emilio Jesus Gallego Arias	2018-06-12
*	Remove some occurrences of Evd.empty	Maxime Dénès	2018-05-25
*	Deprecate Typing.e_* functions	Gaëtan Gilbert	2018-05-14
*	Evar maps contain econstrs.	Gaëtan Gilbert	2018-04-13
*	[located] Push inner locations in `reference` to a CAst.t node.	Emilio Jesus Gallego Arias	2018-03-09
*	Rename some universe minimizing "normalize" functions to "minimize"	Gaëtan Gilbert	2018-03-06
*	Merge PR #6855: Update headers following #6543.	Maxime Dénès	2018-03-05
\|\
* \	Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.	Maxime Dénès	2018-03-04
\|\ \
* \ \	Merge PR #6676: [proofview] goals come with a state	Maxime Dénès	2018-03-04
\|\ \ \
\| \| * \|	[econstr] Continue consolidation of EConstr API under `interp`.	Emilio Jesus Gallego Arias	2018-02-28
\| \|/ / \|/\| \|
\| \| *	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
\| *	proofview: goals come with a state	Enrico Tassi	2018-02-20
\|/
*	Reductionops.nf_* now take an environment.	Gaëtan Gilbert	2018-02-02
*	Remove the local polymorphic flag hack.	Maxime Dénès	2017-12-27
*	Merge PR #6419: [vernac] Split `command.ml` into separate files.	Maxime Dénès	2017-12-18
\|\
\| *	[flags] Make program_mode a parameter for commands in vernac.	Emilio Jesus Gallego Arias	2017-12-17
* \|	Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.	Maxime Dénès	2017-12-14
\|\ \
* \| \|	[proof] Embed evar_map in RefinerError exception.	Emilio Jesus Gallego Arias	2017-12-11
\| \|/ \|/\|
\| *	[lib] Rename Profile to CProfile	Emilio Jesus Gallego Arias	2017-12-09
\|/
*	Use Entries.constant_universes_entry more.	Gaëtan Gilbert	2017-11-24
*	When declaring constants/inductives use ContextSet if monomorphic.	Gaëtan Gilbert	2017-11-24
*	Stop exposing UState.universe_context and its Evd wrapper.	Gaëtan Gilbert	2017-11-24
*	Separate checking univ_decls and obtaining universe binder names.	Gaëtan Gilbert	2017-11-24
*	[plugin] Remove LocalityFixme über hack.	Emilio Jesus Gallego Arias	2017-11-22
*	[api] Another large deprecation, `Nameops`	Emilio Jesus Gallego Arias	2017-11-13
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	[ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.	Emilio Jesus Gallego Arias	2017-10-05
*	Efficient fresh name generation relying on sets.	Pierre-Marie Pédrot	2017-09-28
*	Don't lose names in UState.universe_context.	Gaëtan Gilbert	2017-09-19
*	deprecate Pp.std_ppcmds type alias	Matej Košík	2017-07-27
*	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias	2017-07-17
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Dualize the unsafe flag of refine into typecheck and make it mandatory.	Pierre-Marie Pédrot	2017-06-13
*	Remove (useless) aliases from the API.	Matej Košík	2017-06-10
*	Put all plugins behind an "API".	Matej Kosik	2017-06-07
*	Remove the Sigma (monotonous state) API.	Maxime Dénès	2017-06-06
*	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
*	Ltac cleanup: no more constr_of_global calls	Matthieu Sozeau	2017-05-29
*	Merge PR#512: [cleanup] Unify all calls to the error function.	Maxime Dénès	2017-05-29
\|\
\| *	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias	2017-05-27
* \|	[coqlib] Move `Coqlib` to `library/`.	Emilio Jesus Gallego Arias	2017-05-27
\|/
*	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\
\| *	Post-rebase warnings (unused opens and 2 unused values)	Gaetan Gilbert	2017-04-27
\| *	Fix 4.04 warnings	Gaetan Gilbert	2017-04-27
* \|	[location] [ast] Switch Constrexpr AST to an extensible node type.	Emilio Jesus Gallego Arias	2017-04-25
* \|	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias	2017-04-25
* \|	[location] Use located in tactics.	Emilio Jesus Gallego Arias	2017-04-24