coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Hints API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Tactics API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Clenv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Tacmach 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
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-29
\|\
\| *	Merge remote-tracking branch 'github/pr/321' into v8.6	Maxime Dénès	2016-10-28
\| \|\
\| * \|	Using msg_info for info_auto and info_eauto (PR #324).	Hugo Herbelin	2016-10-26
\| \| *	sections/hints: prevent Not_found in get_type_of	Matthieu Sozeau	2016-10-21
\| \|/
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-17
\|\\|
\| *	Fixing English typography for colon.	Hugo Herbelin	2016-10-14
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-02
\|\\|
\| *	Merge branch 'v8.5' into v8.6	Maxime Dénès	2016-09-30
\| \|\
* \| \|	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
* \| \|	Merge PR #244.	Pierre-Marie Pédrot	2016-09-08
\|\ \ \ \| \|/ / \|/\| \|
* \| \|	Do not normalize evars in Eauto.e_give_exact.	Pierre-Marie Pédrot	2016-09-04
\| * \|	Make the user_err header an optional parameter.	Emilio Jesus Gallego Arias	2016-08-19
\| * \|	Remove errorlabstrm in favor of user_err	Emilio Jesus Gallego Arias	2016-08-19
\|/ /
* \|	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-27
\|\\|
* \|	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
* \|	Put the "exact" family of tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
* \|	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-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
* \|	Removing useless grammar.cma dependencies.	Pierre-Marie Pédrot	2016-03-06
* \|	Moving Eauto to a simple ML file.	Pierre-Marie Pédrot	2016-03-06
\|/
*	Fichiers tactics/.ml4 remplacent les tactics/.v	herbelin	2002-05-29
*	compat ocaml 3.03	filliatr	2001-12-13
*	nouvel algo de conversion plus uniforme	barras	2001-11-29
*	Diverses petites simplications de la machine de preuves.	clrenard	2001-11-19
*	GROS COMMIT:	barras	2001-11-05
*	Autoriser Apply avec un but sous forme d'implication ou de quantification	barras	2001-06-29
*	amelioration des messages d'erreurs vis a vis des evars	barras	2001-05-23
*	amelioration de la structure des univers	barras	2001-03-28
*	entetes	filliatr	2001-03-15
*	changement comparaison etats	filliatr	2001-03-08
*	Modification de e_give_exact pour eviter d'echouer sur l'unification	mohring	2001-03-06
*	eta-expansion	mohring	2001-03-06
*	EAutod (debug)	filliatr	2001-03-06
*	module Explore générique et réécriture EAuto avec ce module; occur check ...	filliatr	2001-03-05
*	modif	mohring	2001-02-28
*	EAuto mixte (largeur puis profondeur)	mohring	2001-02-27
*	Eauto version en largeur	mohring	2001-02-26
*	Reparation IsMutConstruct + Transparent	mohring	2000-11-23
*	suppression des (* open Generic *)	filliatr	2000-11-02
*	Suppression du test de convertibilite inutile pour la plupart des exact; 2 ve...	herbelin	2000-10-13
*	Prise en compte de l'env local dans make_apply_entry	herbelin	2000-10-11