coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Removing a normalization hotspot from EConstr.	Pierre-Marie Pédrot	2017-04-05
*	Merge branch 'trunk' into pr379	Maxime Dénès	2017-04-04
\|\
\| *	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-04-03
\| \|\
\| \| *	Merge PR#533: Instances should obey universe binders even when defined by tac...	Maxime Dénès	2017-04-03
\| \| \|\
\| * \| \|	Fix loading of ocamldebug printers.	Pierre-Marie Pédrot	2017-04-03
\| \| \| *	Instances should obey universe binders even when defined by tactics.	Gaetan Gilbert	2017-04-03
\| \| \|/
\| * \|	Merge PR#417: No cast surgery in let in	Maxime Dénès	2017-04-03
\| \|\ \
\| \| \| *	Add test file for #4957.	Maxime Dénès	2017-04-03
\| * \| \|	Fix higher-order pattern variables not being printed as "@?" (bug #5431).	Guillaume Melquiond	2017-04-02
\| * \| \|	Fix documentation typo (bug #5433).	Guillaume Melquiond	2017-04-02
\| * \| \|	Simplify some proofs.	Guillaume Melquiond	2017-04-02
* \| \| \|	Restore a fast path in EConstr instance normalization.	Pierre-Marie Pédrot	2017-04-01
* \| \| \|	Using delayed universe instances in EConstr.	Pierre-Marie Pédrot	2017-04-01
\| * \| \|	Declaring ltac plugin, so that static linking works.	Hugo Herbelin	2017-04-01
* \| \| \|	Actually exporting delayed universes in the EConstr implementation.	Pierre-Marie Pédrot	2017-04-01
* \| \| \|	Make the Constr.kind_of_term type parametric in sorts and universes.	Pierre-Marie Pédrot	2017-03-31
* \| \| \|	Ensuring proper cast invariants in EConstr.kind.	Pierre-Marie Pédrot	2017-03-31
* \| \| \|	Revert "Specially crafted EConstr.kind to be more efficient."	Pierre-Marie Pédrot	2017-03-31
* \| \| \|	Specially crafted EConstr.kind to be more efficient.	Pierre-Marie Pédrot	2017-03-30
\| * \| \|	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-03-30
\| \|\ \ \ \| \| \| \|/ \| \| \|/\|
\| \| * \|	Merge PR#463: Run non-tactic comands without resilient_command	Maxime Dénès	2017-03-30
\| \| \|\ \
\| * \| \| \|	Fix ring_simplify sometimes producing R0 and R1 instead of 0%R and 1%R.	Guillaume Melquiond	2017-03-30
\| * \| \| \|	Merge PR#469: Added take to VectorDef	Maxime Dénès	2017-03-30
\| \|\ \ \ \
\| \| * \| \| \|	Added take to VectorDef.	George Stelle	2017-03-30
\| * \| \| \| \|	Merge PR#511: [stm] Remove some obsolete vernacs/classification.	Maxime Dénès	2017-03-30
\| \|\ \ \ \ \
\| * \ \ \ \ \	Merge PR#522: [coqide] Protect against size_allocate race in proofview.	Maxime Dénès	2017-03-29
\| \|\ \ \ \ \ \
\| * \ \ \ \ \ \	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-03-29
\| \|\ \ \ \ \ \ \ \| \| \| \|_\|_\|/ / / \| \| \|/\| \| \| \| \|
\| \| * \| \| \| \| \|	Merge PR#514: [travis] Backport from trunk: VST	Maxime Dénès	2017-03-29
\| \| \|\ \ \ \ \ \
\| * \| \ \ \ \ \ \	Merge PR#506: [nit] Fix a couple incorrect uses of msg_error.	Maxime Dénès	2017-03-29
\| \|\ \ \ \ \ \ \ \
\| * \ \ \ \ \ \ \ \	Merge PR#521: Do so that "About" tells if a reference is a coercion.	Maxime Dénès	2017-03-29
\| \|\ \ \ \ \ \ \ \ \
\| * \ \ \ \ \ \ \ \ \	Merge PR#525: [ide] Fix typo in pp serialization.	Maxime Dénès	2017-03-29
\| \|\ \ \ \ \ \ \ \ \ \
* \| \| \| \| \| \| \| \| \| \| \|	Merge branch 'trunk' into pr379	Maxime Dénès	2017-03-29
\|\\| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \|	Fix call to broken unsafe_type_of in apply tactic.	Maxime Dénès	2017-03-29
\| \| \| \| \| \| \| \| \| \| * \|	Run non-tactic comands without resilient_command	Tej Chajed	2017-03-29
\| \| \| \| \| \| \|_\|_\|_\|/ / \| \| \| \| \| \|/\| \| \| \| \|
\| \| * \| \| \| \| \| \| \| \|	[ide] Fix typo in pp serialization.	Emilio Jesus Gallego Arias	2017-03-29
* \| \| \| \| \| \| \| \| \| \|	Revert to incorrect heuristic in apply.	Maxime Dénès	2017-03-28
\| * \| \| \| \| \| \| \| \| \|	Fixing missing PropFacts.v in Logic/vo.itarget.	Hugo Herbelin	2017-03-28
\| \|/ / / / / / / / /
\| \| \| \| \| \| * / / /	[coqide] Protect against size_allocate race in proofview.	Emilio Jesus Gallego Arias	2017-03-28
\| \| \|_\|_\|_\|/ / / / \| \|/\| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \|	Do so that "About" tells if a reference is a coercion.	Hugo Herbelin	2017-03-27
\| \|/ / / / / / /
* \| \| \| \| \| \| \|	Mathcomp overlay.	Maxime Dénès	2017-03-25
* \| \| \| \| \| \| \|	Fix interpretation of Ltac patterns episode 2.	Maxime Dénès	2017-03-24
* \| \| \| \| \| \| \|	Merge branch 'trunk' into pr379	Maxime Dénès	2017-03-24
\|\\| \| \| \| \| \| \|
\| \| \| \| * \| \| \|	[travis] Backport from trunk: VST	Emilio Jesus Gallego Arias	2017-03-24
\| \| \| \|/ / / /
\| * \| \| \| \| \|	Merge PR#489: [travis] Add VST	Maxime Dénès	2017-03-24
\| \|\ \ \ \ \ \
\| \| \| \| \| * \| \|	[stm] Remove some obsolete vernacs/classification.	Emilio Jesus Gallego Arias	2017-03-24
\| \| \| * \| \| \| \|	[nit] Fix a couple incorrect uses of msg_error.	Emilio Jesus Gallego Arias	2017-03-24
\| \| \| \| \|/ / / \| \| \| \|/\| \| \|
\| \| * / \| \| \|	[travis] Add VST	Emilio Jesus Gallego Arias	2017-03-24
\| \| \|/ / / /
\| \| \| \| \| *	Applying same convention as in Definition for printing type in a let in.	Hugo Herbelin	2017-03-24
\| \| \| \| \| *	Applying same convention as in Definition for parsing type in a let in.	Hugo Herbelin	2017-03-24
\| \| \| \| \| *	Documenting main changes of API.	Hugo Herbelin	2017-03-24