coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| \| * \| \| \| \| \| \|	Fix bug #5501: Universe polymorphism breaks proof involving auto.	Pierre-Marie Pédrot	2017-04-30
\| \|/ / / / / / / \|/\| \| \| \| \| \| \|
\| \| \| \| \| * \| \|	Fixing "decide equality"'s bug #5449.	Hugo Herbelin	2017-04-30
\| \|_\|_\|_\|/ / / \|/\| \| \| \| \| \|
* \| \| \| \| \| \|	Suppress warning message in stdlib.	Guillaume Melquiond	2017-04-29
* \| \| \| \| \| \|	Revert "Renaming allow_patvar flag of intern_gen into pattern_mode."	Maxime Dénès	2017-04-28
* \| \| \| \| \| \|	Revert "Using a more explicit algebraic type for evars of kind "MatchingVar"."	Maxime Dénès	2017-04-28
\| \| \| \| * \| \|	Allow interactive editing of {C,}Morphisms in PG	Jason Gross	2017-04-28
\| \|_\|_\|/ / / \|/\| \| \| \| \|
\| \| \| * \| \|	Add .dir-locals.el and _CoqProject files for emacs stdlib editing	Jason Gross	2017-04-28
\| \|_\|/ / / \|/\| \| \| \|
* \| \| \| \|	Using a more explicit algebraic type for evars of kind "MatchingVar".	Hugo Herbelin	2017-04-28
* \| \| \| \|	Renaming allow_patvar flag of intern_gen into pattern_mode.	Hugo Herbelin	2017-04-28
* \| \| \| \|	Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...	Maxime Dénès	2017-04-28
\|\ \ \ \ \
\| \| * \| \| \|	Post-rebase warnings (unused opens and 2 unused values)	Gaetan Gilbert	2017-04-27
\| \| * \| \| \|	Enable more warnings, and add -warn-error configure flag	Gaetan Gilbert	2017-04-27
\| \| * \| \| \|	Fix 4.04 warnings	Gaetan Gilbert	2017-04-27
\| \| * \| \| \|	Remove uses of [Flags.make_silent]	Gaetan Gilbert	2017-04-27
\| \| * \| \| \|	Warning 29: non escaped end of line may be non portable	Gaetan Gilbert	2017-04-27
\| \| * \| \| \|	Remove unused [open] statements	Gaetan Gilbert	2017-04-27
\| \| * \| \| \|	Micromega: do not use Filename.temp_dir_path, remove unused values	Gaetan Gilbert	2017-04-27
\| \| * \| \| \|	Remove unused constructors	Gaetan Gilbert	2017-04-27
\| \| * \| \| \|	Add [_] prefix to unused values which maybe should be kept	Gaetan Gilbert	2017-04-27
\| \| * \| \| \|	Remove some unused values and types	Gaetan Gilbert	2017-04-27
\| \| * \| \| \|	Rename Sos_lib.(\|\|) -> parser_or to avoid (deprecated) Pervasives.or	Gaetan Gilbert	2017-04-27
\| \| * \| \| \|	Disambiguate Polynomial.Hyp and Mfourier.Hyp -> Assum	Gaetan Gilbert	2017-04-27
\| \| * \| \| \|	Use [method!] to override methods (warning 7)	Gaetan Gilbert	2017-04-27
\| \| * \| \| \|	Fix omitted labels in function calls	Gaetan Gilbert	2017-04-27
\| \| * \| \| \|	Remove unused [rec] keywords	Gaetan Gilbert	2017-04-27
\| \| * \| \| \|	Locally disable some warnings.	Gaetan Gilbert	2017-04-27
* \| \| \| \| \|	Merge PR#414: Some more theory on powerRZ.	Maxime Dénès	2017-04-27
\|\ \ \ \ \ \ \| \|_\|/ / / / \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR#583: [toplevel] More work on error handling.	Maxime Dénès	2017-04-27
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR#586: trivial cleanup commits which does not change Coq API	Maxime Dénès	2017-04-27
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR#568: Remove tactic compatibility layer	Maxime Dénès	2017-04-27
\|\ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \|	Document the API changes.	Pierre-Marie Pédrot	2017-04-27
* \| \| \| \| \| \| \| \|	Merge PR#584: Give andb_prop a simpler proof	Maxime Dénès	2017-04-27
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR#585: Small typo in comment	Maxime Dénès	2017-04-27
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-04-27
\|\ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| * \| \| \| \| \| \|	contracting the type of "Pfedit.solve_by_implicit_tactic"	Matej Košík	2017-04-27
\| \|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \| \|	Small typo in comment	Vadim Zaliva	2017-04-26
\| \|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| *	transparent abstract: Respond to review comment	Jason Gross	2017-04-25
\| \| \| \| \| \| \| \| \| *	transparent abstract: Respond to review comment	Jason Gross	2017-04-25
\| \| \| \| \| \| \| \| \| *	Make opaque optional only for tclABSTRACT	Jason Gross	2017-04-25
\| \| \| \| \| \| \| \| \| *	Generalize cache_term_by_tactic_then	Jason Gross	2017-04-25
\| \| \| \| \| \| \| \| \| *	Mark transparent_abstract as risky in docs	Jason Gross	2017-04-25
\| \| \| \| \| \| \| \| \| *	Add transparent_abstract tactic	Jason Gross	2017-04-25
\| \| \| \| \| \| \| \| \| *	Add support for transparent abstract (no syntax)	Jason Gross	2017-04-25
\| \|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \|	Give andb_prop a simpler proof	Jason Gross	2017-04-25
\| \|/ / / / / / / \|/\| \| \| \| \| \| \|
\| \| \| * \| \| \| \|	[toplevel] Remove unused parameter from `Vernac.process_expr`.	Emilio Jesus Gallego Arias	2017-04-25
\| \| \| * \| \| \| \|	[toplevel] Use exception information for error printing.	Emilio Jesus Gallego Arias	2017-04-25
\| * \| \| \| \| \| \|	Fix an optimization failure in tclPROGRESS.	Pierre-Marie Pédrot	2017-04-25
* \| \| \| \| \| \| \|	Fix an optimization failure in tclPROGRESS.	Pierre-Marie Pédrot	2017-04-25
\| * \| \| \| \| \| \|	Merge PR#567: Fix bug #5377: @? patterns broken.	Maxime Dénès	2017-04-25
\| \|\ \ \ \ \ \ \
* \| \ \ \ \ \ \ \	Merge PR#578: Fix nsatz not recognizing real literals.	Maxime Dénès	2017-04-25
\|\ \ \ \ \ \ \ \ \