coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Factor interp_instance out of Pretyping.pretype_global	Gaetan Gilbert	2017-04-06
*	Avoid strange shadowing of Pretyping.interp_universe_level_name	Gaetan Gilbert	2017-04-06
*	Merge PR#434: Optimizing array mapping in the kernel.	Maxime Dénès	2017-04-05
\|\
* \	Merge PR#502: [pp] Add anomaly header to error messages.	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
* \| \| \| \|	Declaring ltac plugin, so that static linking works.	Hugo Herbelin	2017-04-01
* \| \| \| \|	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
\|\ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| * \| \| \|	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
* \| \| \| \| \| \| \| \| \| \| \|	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
\|/ / / / / / / / /
\| \| \| * / / / / /	[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
\| \| \| \| * \| \|	Replacing "cast surgery" in LetIn by a proper field (see PR #404).	Hugo Herbelin	2017-03-24
\| \| \| \| * \| \|	Using the same type of binders for interning and externing.	Hugo Herbelin	2017-03-24
\| \| \| \| * \| \|	Unifying standard "constr_level" names for constructors of local_binder_expr.	Hugo Herbelin	2017-03-24
\| \| \| \| * \| \|	Renaming local_binder into local_binder_expr.	Hugo Herbelin	2017-03-24
\| \| \| \| * \| \|	Merging glob_binder and glob_decl.	Hugo Herbelin	2017-03-24
\| \| \| \| * \| \|	Type extended_glob_local_binder now contains only glob_constr.	Hugo Herbelin	2017-03-24
\| \| \| \| * \| \|	Standardized the order of constructors for binders: Assum then Def.	Hugo Herbelin	2017-03-24
\| \| \| \| * \| \|	Cleaning phase around local binder at glob level:	Hugo Herbelin	2017-03-24
\| \| \| \| * \| \|	"Standardizing" the name LocalPatten into LocalRawPattern.	Hugo Herbelin	2017-03-24
\| \|_\|_\|/ / / \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR#392: strengthened the statement of JMeq_eq_dep	Maxime Dénès	2017-03-24
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-03-24
\|\ \ \ \ \ \ \ \| \| \|_\|/ / / / \| \|/\| \| \| \| \|