coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Make direct invocations of `simple apply` obey `Opaque` directive.	Maxime Dénès	2018-06-05
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Remove the Sigma (monotonous state) API.	Maxime Dénès	2017-06-06
*	unification.mli: Fix a spelling typo in a comment	Jason Gross	2017-05-23
*	Merge branch 'master' into econstr	Pierre-Marie Pédrot	2017-04-07
\|\
\| *	Ensuring static invariants about handling of pending evars in Pretyping.	Pierre-Marie Pédrot	2017-03-23
* \|	Definining EConstr-based contexts.	Pierre-Marie Pédrot	2017-02-14
* \|	Unification API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|/
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-13
\|\\|
\| *	Fix essential bug in new Keyed Unification mode reported by R. Krebbers.	Matthieu Sozeau	2016-01-12
* \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \|	More monotonicity in Tactics.	Pierre-Marie Pédrot	2015-10-19
\|/
*	Update headers.	Maxime Dénès	2015-01-12
*	Follow up to experimental eager evar unification in bcba6d1bc9:	Hugo Herbelin	2014-11-08
*	Enlarge the cases where the like first selection is used in destruct.	Hugo Herbelin	2014-10-31
*	Fixing destruct/induction with a using clause on a non-inductive type,	Hugo Herbelin	2014-10-26
*	This commit introduces changes in induction and destruct.	Hugo Herbelin	2014-10-25
*	A step towards better differentiating when w_unify is used for subterm	Hugo Herbelin	2014-09-10
*	Made the subterm finding function make_abstraction independent of the	Hugo Herbelin	2014-06-28
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Removing dead code, thanks to new OCaml warnings and a bit of scripting.	Pierre-Marie Pédrot	2014-04-23
*	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot	2013-09-18
*	export Unification.abstract_list_all_with_dependencies	pboutill	2013-05-30
*	Fixed a little inefficiency of "set/destruct" over a pattern. Now	herbelin	2012-12-18
*	Improving error message when abtraction over goal (abstract_list_all	herbelin	2012-10-04
*	Updating headers.	herbelin	2012-08-08
*	Added a flag to control the use of typing when instantiating applied	herbelin	2011-12-17
*	Moved to a more standard order of arguments (i.e. env followed by evar_map)	herbelin	2011-10-11
*	Fix unification: detect invalid evar instantiations due to scoping earlier.	msozeau	2011-08-04
*	Generalizing flag use_evars_pattern_unification into a flag	herbelin	2011-06-18
*	Added a flag to restrict conversion in tactic unification on the	herbelin	2011-06-13
*	Added a new flag for freezing evars in tactic unification. Used this	herbelin	2011-06-12
*	Moved allow_K to a unification flag	herbelin	2011-06-10
*	Add a flag to control betaiota reduction during unification to maintain backw...	msozeau	2011-04-18
*	- Add modulo_delta_types flag for unification to allow full	msozeau	2011-03-13
*	Added eta-expansion in kernel, type inference and tactic unification,	herbelin	2010-09-20
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	New script dev/tools/change-header to automatically update Coq files headers.	herbelin	2010-06-22
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill	2010-04-29
*	Promote evar_defs to evar_map (in Evd)	glondu	2009-11-11
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Reactivation of pattern unification of evars in apply unification, in	herbelin	2009-07-08
*	Add new variants of [rewrite] and [autorewrite] which differ in the	msozeau	2009-06-30
*	Minor unification changes:	msozeau	2009-05-18
*	- Backtrack sur option with_types suite à confusion sur l'utilisation	herbelin	2008-04-27