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
\| \| *	Document differences of Hint Resolve and Hint Extern	Matthieu Sozeau	2016-02-23
\| \| *	Fix part of bug #4533: respect declared global transparency of	Matthieu Sozeau	2016-02-23
\| \| *	Fix bug #4544: Backtrack on using full betaiota reduction during keyed unific...	Matthieu Sozeau	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