coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Using delayed universe instances in EConstr.	Pierre-Marie Pédrot	2017-04-01
*	Merge branch 'master'.	Pierre-Marie Pédrot	2017-02-14
\|\
* \|	Removing most nf_enter in tactics.	Pierre-Marie Pédrot	2017-02-14
* \|	Definining EConstr-based contexts.	Pierre-Marie Pédrot	2017-02-14
* \|	Removing compatibility layers from Tacticals	Pierre-Marie Pédrot	2017-02-14
* \|	Removing various compatibility layers of tactics.	Pierre-Marie Pédrot	2017-02-14
* \|	Proofview.Goal primitive now return EConstrs.	Pierre-Marie Pédrot	2017-02-14
* \|	Elim API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Tactics API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Tacticals 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
* \|	Retyping API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Termops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| *	Proofview: tclINDEPENDENTL	Enrico Tassi	2017-02-10
\|/
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-17
\|\
\| *	Fix bug #5139: Anomalies should not be caught by \|\| / try.	Pierre-Marie Pédrot	2016-10-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
* \|	Merge PR #244.	Pierre-Marie Pédrot	2016-09-08
\|\ \
* \| \|	CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...	Matej Kosik	2016-08-30
* \| \|	CLEANUP: minor readability improvements	Matej Kosik	2016-08-24
\| \|/ \|/\|
\| *	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
\| *	Unify location handling of error functions.	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
*	Optimize the subst tactic.	Pierre-Marie Pédrot	2016-06-24
*	Goal selectors are now tacticals and can be used as such.	Cyprien Mangin	2016-06-14
*	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
*	New step on recent 9c2662eecc398f3 (strong invariants on tuple pattern).	Hugo Herbelin	2016-01-21
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
* \|	Stronger invariants on the use of the introduction pattern (pat1,...,patn).	Hugo Herbelin	2016-01-21
* \|	Fixing some problems with double induction.	Hugo Herbelin	2016-01-21
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	merge	Matej Kosik	2016-01-11
\|\ \
\| * \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \| \|	Tentative API fix for tactic arguments to be fed to tclWITHHOLES.	Pierre-Marie Pédrot	2015-12-27
\|/ /
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-20
\|\\|
\| *	More optimizations of [Clenv.clenv_fchain].	Pierre-Marie Pédrot	2015-11-17
* \|	Removing some goal unsafeness in inductive schemes.	Pierre-Marie Pédrot	2015-10-29
* \|	Proofview.Goal.sigma returns an indexed evarmap.	Pierre-Marie Pédrot	2015-10-20
* \|	Indexing Proofview.goals with a stage.	Pierre-Marie Pédrot	2015-10-20
* \|	Boxing the Goal.enter primitive into a record type.	Pierre-Marie Pédrot	2015-10-20
\|/
*	Univs: fix many evar_map initializations and leaks.	Matthieu Sozeau	2015-10-02
*	Safer typing primitives.	Pierre-Marie Pédrot	2015-05-13
*	Remove almost all the uses of string concatenation when building error messages.	Guillaume Melquiond	2015-04-23
*	Using tclZEROMSG instead of tclZERO in several places.	Pierre-Marie Pédrot	2015-04-23
*	More expressive API for tclWITHHOLES.	Pierre-Marie Pédrot	2015-02-10
*	Removing dead code.	Pierre-Marie Pédrot	2015-02-02
*	Update headers.	Maxime Dénès	2015-01-12