coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Remove unused [open] statements	Gaetan Gilbert	2017-04-27
*	Eauto API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Hints API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Untangling Tacexpr from lower strata.	Pierre-Marie Pédrot	2016-09-15
*	Unplugging Tacexpr in several interface files.	Pierre-Marie Pédrot	2016-09-08
*	Moving Eauto and Class_tactics to tactics/.	Pierre-Marie Pédrot	2016-03-25
*	Creating a dedicated ltac/ folder for Hightactics.	Pierre-Marie Pédrot	2016-03-21
*	Moving Eauto to a simple ML file.	Pierre-Marie Pédrot	2016-03-06
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Reduce dependencies of interface files.	Guillaume Melquiond	2016-01-02
* \|	Eradicating uses of open_constr in TACTIC EXTEND in favour of uconstr.	Pierre-Marie Pédrot	2015-12-28
* \|	Removing auto from the tactic AST.	Pierre-Marie Pédrot	2015-12-24
* \|	Partially porting eauto to the new tactic API.	Pierre-Marie Pédrot	2015-02-23
\|/
*	Removing dead code.	Pierre-Marie Pédrot	2015-02-02
*	Update headers.	Maxime Dénès	2015-01-12
*	Splitting out of auto.ml a file hints.ml dedicated to hints so as to	Hugo Herbelin	2014-10-07
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Cutting the dependency of Genarg in constr_expr, glob_constr	ppedrot	2013-06-21
*	Uniformizing generic argument types.	ppedrot	2013-06-06
*	Updating headers.	herbelin	2012-08-08
*	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey	2012-05-29
*	info_trivial, info_auto, info_eauto, and debug (trivial\|auto)	letouzey	2012-03-30
*	An experimental support for open constrs in hints and in "using"	herbelin	2010-10-31
*	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
*	Add (almost) compatibility with camlp4, without breaking support for camlp5	letouzey	2010-05-19
*	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill	2010-04-29
*	Fix splitting evars tactics and stop dropping evar constraints when	msozeau	2010-03-15
*	Fix [autounfold] to accept general [in] clauses.	msozeau	2010-03-05
*	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau	2009-10-28
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Use the proper unification flags in e_exact. This makes exact fail a bit	msozeau	2009-07-09
*	- Parameterize unification by two sets of transparent_state, one for open	msozeau	2008-04-21
*	correction d'un bug d'efficacite dans Function (+ ajout de eauto_with_bases)	jforest	2008-03-08
*	Backtrack changes on eauto, move specialized version of eauto in	msozeau	2008-02-14
*	Fix the clrewrite tactic, change Relations.v to work on relations in Prop	msozeau	2008-02-09
*	Change implementation of resolution for typeclasses to use a customized	msozeau	2008-02-08
*	Work-in-progress to make eauto accept a list of goals as input and	msozeau	2008-02-06
*	Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.	herbelin	2007-04-28
*	- Correction d'un bug de make_clenv_binding_apply révélé par le commit 9771	herbelin	2007-04-18
*	Export de simplest_eapply, utilisé dans la contrib interface	notin	2007-04-16
*	Suite unification apply et eapply (l'un et l'autre profite maintenant	herbelin	2007-04-16
*	Ajout option 'using lemmas' à auto/trivial/eauto	herbelin	2006-01-28
*	Suppression de la dépendance en Map.fold de ocaml dont la sémantique a	herbelin	2006-01-24
*	A la demande de Julien Forest	letouzey	2005-11-17
*	Nouvelle en-tête	herbelin	2004-07-16
*	Interface Eauto	herbelin	2003-09-18