coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| *	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
*	Fixing #3896 (incorrect sigma given to printer).	Hugo Herbelin	2015-01-03
*	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot	2014-12-16
*	Add Ltac syntax for the [tclIFCATCH] primitive.	Arnaud Spiwack	2014-12-12
*	Tentatively more informative report of failure when inferring	Hugo Herbelin	2014-12-11
*	Constructor tactics backtracking is done using [Tacticals.New] rather than [P...	Arnaud Spiwack	2014-12-08
*	Adding locations to tclZEROMSG.	Pierre-Marie Pédrot	2014-11-20
*	Plural and singular forms in error messages.	Hugo Herbelin	2014-11-02
*	Proofview: split [V82] module into [Unsafe] and [V82].	Arnaud Spiwack	2014-10-22
*	Display number of available goals in "incorrect number of goals" error message.	Arnaud Spiwack	2014-09-08
*	Renaming goal-entering functions.	Pierre-Marie Pédrot	2014-09-06
*	Simplification of the tclCHECKINTERRUPT tactic.	Pierre-Marie Pédrot	2014-08-28
*	Lazy interpretation of patterns so that expressions such as "intros H H'/H"	Hugo Herbelin	2014-08-18
*	Adding a new intro-pattern for "apply in" on the fly. Using syntax	Hugo Herbelin	2014-08-18
*	Improving error message when applying rewrite to an expression which is not a...	Hugo Herbelin	2014-08-18
*	Reorganisation of intropattern code	Hugo Herbelin	2014-08-18
*	More self-contained code for tclWITHHOLES.	Pierre-Marie Pédrot	2014-08-15
*	Adding a "time" tactical for benchmarking purposes. In case the tactic	Hugo Herbelin	2014-07-13
*	check_for_interrupt: better (but slower) in threading mode	Enrico Tassi	2014-07-10
*	Revert "time tac" (committed by mistake).	Hugo Herbelin	2014-07-07
*	time tac	Hugo Herbelin	2014-07-07
*	Clenvtac.clenv_refine in the new monad. Not satisfactory though, because it	Pierre-Marie Pédrot	2014-06-24
*	Removing opens to Clenvtac to track its use more easily.	Pierre-Marie Pédrot	2014-06-23