coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Getting rid of the "<:tactic< ... >>" quotations.	Pierre-Marie Pédrot	2016-02-24
*	Moving tauto.ml4 to a proper ML file.	Pierre-Marie Pédrot	2016-02-23
*	Moving the Tauto tactic to proper Ltac.	Pierre-Marie Pédrot	2016-02-22
*	The tactic generic argument now returns a value rather than a glob_expr.	Pierre-Marie Pédrot	2016-02-22
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-02-21
\|\
\| *	Fixing bug #4540: CoqIDE bottom progress bar does not update.	Pierre-Marie Pédrot	2016-02-20
\| *	Fix regression from 8.4 in reflexivity/...	Matthieu Sozeau	2016-02-19
* \|	Merge branch 'located-universes'	Pierre-Marie Pédrot	2016-02-19
\|\ \
\| * \|	Adding location to universes generated by the pretyper.	Pierre-Marie Pédrot	2016-02-19
\| * \|	Allowing to attach location to universes in UState.	Pierre-Marie Pédrot	2016-02-19
\|/ /
\| *	Fixing bug #4580: [Set Refine Instance Mode] also used for Program Instance.	Pierre-Marie Pédrot	2016-02-19
\| *	Fixing bug #4582: cannot override notation [ x ].	Pierre-Marie Pédrot	2016-02-19
\| *	STM: Print/Extraction have to be skipped if -quick	Enrico Tassi	2016-02-19
\| *	CoqIDE: STOP button also stops workers (fix #4542)	Enrico Tassi	2016-02-19
\| *	STM: classify some variants of Instance as regular `Fork nodes.	Enrico Tassi	2016-02-19
* \|	FIX: of my previous merging mistake	Matej Kosik	2016-02-18
* \|	ADD: Names.Name.is_{anonymous,name}	Matej Kosik	2016-02-18
\| *	Fixing the Proofview.Goal.goal function.	Pierre-Marie Pédrot	2016-02-17
\| *	Fix bug #4574: Anomaly: Uncaught exception Invalid_argument("splay_arity").	Pierre-Marie Pédrot	2016-02-17
* \|	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-17
\|\ \
* \| \|	CLEANUP: Renaming "Util.compose" function to "%"	Matej Kosik	2016-02-17
* \| \|	Tacticals: typo in a comment	Pierre Letouzey	2016-02-16
* \| \|	Term: fix a comment (first de Bruijn index is 1)	Pierre Letouzey	2016-02-16
\| * \|	Renaming variants of Entries.local_entry	Matej Kosik	2016-02-16
\| * \|	CLEANUP: Simplifying the changes done in "checker/*"	Matej Kosik	2016-02-15
\| * \|	merging conflicts with the original "trunk__CLEANUP__Context__2" branch	Matej Kosik	2016-02-15
\|/\| \|
* \| \|	Using monotonic types for conversion functions.	Pierre-Marie Pédrot	2016-02-15
\| * \|	CLEANUP: Simplifying the changes done in "kernel/*"	Matej Kosik	2016-02-15
* \| \|	Code factorization of tactic "unfold_body".	Pierre-Marie Pédrot	2016-02-15
* \| \|	More conversion functions in the new tactic API.	Pierre-Marie Pédrot	2016-02-15
* \| \|	Moving conversion functions to the new tactic API.	Pierre-Marie Pédrot	2016-02-15
* \| \|	Renaming functions in Typing to stick to the standard e_* scheme.	Pierre-Marie Pédrot	2016-02-15
* \| \|	Monotonizing the Evarutil module.	Pierre-Marie Pédrot	2016-02-15
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-02-13
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	Do not give a name to anonymous evars anymore. See bug #4547.	Pierre-Marie Pédrot	2016-02-13
\| * \|	STM: always stock in vio files the first node (state) of a proof	Enrico Tassi	2016-02-10
\| * \|	STM: not delegate proofs that contain Vernac(Module\|Require\|Import), #4530	Enrico Tassi	2016-02-10
\| * \|	Don't fail fatally if PATH is not set.	Emilio Jesus Gallego Arias	2016-02-10
\| \| *	REFORMATTING: kernel/context.ml{,i}	Matej Kosik	2016-02-09
\| \| *	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
\| \|/ \|/\|
\| *	Improving error message with missing patterns in the presence of	Hugo Herbelin	2016-02-08
\| *	Optimizing the universes_of_constr_function.	Pierre-Marie Pédrot	2016-02-03
\| *	Optimizing the computation of frozen evars.	Pierre-Marie Pédrot	2016-02-03
* \|	Adding a "get" primitive to map signature.	Pierre-Marie Pédrot	2016-02-03
\| *	Opacifying the type of evar naming structure in Evd.	Pierre-Marie Pédrot	2016-02-03
\| *	More compact representation for evar resolvability flag.	Pierre-Marie Pédrot	2016-02-03
* \|	Removing a source of type-unsafeness in Pcoq.	Pierre-Marie Pédrot	2016-02-02
* \|	Infering atomic ML entries from their grammar.	Pierre-Marie Pédrot	2016-02-01
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-29
\|\\|
\| *	Fix bug #4537: Coq 8.5 is slower in typeclass resolution.	Pierre-Marie Pédrot	2016-01-27