coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Decompiling pattern-matching: mini-removal dead code.	Hugo Herbelin	2017-12-12
*	In printing, factorizing "match" clauses with same right-hand side.	Hugo Herbelin	2017-12-12
*	Proper nametab handling of global universe names	Matthieu Sozeau	2017-12-01
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	[general] Remove Econstr dependency from `intf`	Emilio Jesus Gallego Arias	2017-10-25
*	Merge PR #1084: After testing it in live, writing metas using an ?INTERNAL#42...	Maxime Dénès	2017-10-03
\|\
* \|	Efficient computation of the names contained in an environment.	Pierre-Marie Pédrot	2017-09-28
* \|	Efficient fresh name generation relying on sets.	Pierre-Marie Pédrot	2017-09-28
\| *	After testing it in live, writing metas using an ?INTERNAL#42 style is ugly.	Hugo Herbelin	2017-09-23
\|/
*	Proposing meta names more distinguishable from evar names than ?M42.	Hugo Herbelin	2017-09-21
*	A possible fix to BZ#5750 (ability to print context of ltac subterm match).	Hugo Herbelin	2017-09-21
*	Making detyping potentially lazy.	Pierre-Marie Pédrot	2017-09-04
*	Prevent overallocation in Array.map_to_list and remove custom implementation ...	Guillaume Melquiond	2017-08-22
*	Merge PR #913: Less allocations in Detyping	Maxime Dénès	2017-08-01
\|\
* \|	deprecate Pp.std_ppcmds type alias	Matej Košík	2017-07-27
\| *	Add a comment regarding the specialization of the combinator in Detyping.	Pierre-Marie Pédrot	2017-07-26
\| *	Allocation-friendly detyping of term arrays.	Pierre-Marie Pédrot	2017-07-21
\|/
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
*	Don't double up on periods in anomalies	Jason Gross	2017-06-02
*	Creating a module Nameops.Name extending module Names.Name.	Hugo Herbelin	2017-05-31
*	Merge PR#481: [option] Remove support for non-synchronous options.	Maxime Dénès	2017-05-25
\|\
* \	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\ \
\| \| *	[option] Remove support for non-synchronous options.	Emilio Jesus Gallego Arias	2017-05-24
\| \|/
\| *	Merge PR#544: Anonymous universes	Maxime Dénès	2017-05-05
\| \|\
\| \| *	Allow flexible anonymous universes in instances and sorts.	Gaetan Gilbert	2017-05-03
\| * \|	applied the patch for printing types of let bindings by @herbelin	Abhishek Anand (@brixpro-home)	2017-05-02
\| \|/
\| *	Remove unused [open] statements	Gaetan Gilbert	2017-04-27
* \|	[location] [ast] Port module AST to CAst	Emilio Jesus Gallego Arias	2017-04-25
* \|	[location] Make location optional in Loc.located	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
* \|	[location] Move Glob_term.predicate_pattern to located.	Emilio Jesus Gallego Arias	2017-04-24
* \|	[location] Move Glob_term.cases_pattern to located.	Emilio Jesus Gallego Arias	2017-04-24
\|/
*	Merge PR#379: Introducing evar-insensitive constrs	Maxime Dénès	2017-04-11
\|\
* \|	Turning the printing primitive projection parameter flag off by default.	Hugo Herbelin	2017-04-07
* \|	Turning the printing primitive projection compatibility flag off by default.	Hugo Herbelin	2017-04-07
\| *	Merge branch 'trunk' into pr379	Maxime Dénès	2017-04-04
\| \|\ \| \|/ \|/\|
\| *	Using delayed universe instances in EConstr.	Pierre-Marie Pédrot	2017-04-01
\| *	Actually exporting delayed universes in the EConstr implementation.	Pierre-Marie Pédrot	2017-04-01
* \|	Replacing "cast surgery" in LetIn by a proper field (see PR #404).	Hugo Herbelin	2017-03-24
\| *	Namegen primitives now apply on evar constrs.	Pierre-Marie Pédrot	2017-02-14
\| *	Moving printing code from Evd to Termops.	Pierre-Marie Pédrot	2017-02-14
\| *	Removing compatibility layers in Retyping	Pierre-Marie Pédrot	2017-02-14
\| *	Removing some return type compatibility layers in Termops.	Pierre-Marie Pédrot	2017-02-14
\| *	Eliminating parts of the right-hand side compatibility layer	Pierre-Marie Pédrot	2017-02-14
\| *	Tactic_matching API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| *	Tactics API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| *	Cleaning up opening of the EConstr module in pretyping folder.	Pierre-Marie Pédrot	2017-02-14
\| *	Retyping API using EConstr.	Pierre-Marie Pédrot	2017-02-14