coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
\| *	Reductionops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| *	Termops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|/
*	Make the user_err header an optional parameter.	Emilio Jesus Gallego Arias	2016-08-19
*	Unify location handling of error functions.	Emilio Jesus Gallego Arias	2016-08-19
*	Two protections against failures when printing evar_map.	Hugo Herbelin	2016-08-17
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	A new infrastructure for warnings.	Maxime Dénès	2016-06-29
*	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
*	merging conflicts with the original "trunk__CLEANUP__Context__2" branch	Matej Kosik	2016-02-15
\|\
* \	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-02-13
\|\ \
\| * \|	Do not give a name to anonymous evars anymore. See bug #4547.	Pierre-Marie Pédrot	2016-02-13
\| \| *	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
\| \|/ \|/\|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-03
\|\\|
\| *	Add an option to deactivate compatibility printing of primitive	Matthieu Sozeau	2015-12-02
* \|	Experimenting printing the type of the defined term of a LetIn when	Hugo Herbelin	2015-11-07
\|/