coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.	Hugo Herbelin	2018-02-20
*	Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`	Maxime Dénès	2018-02-19
\|\
* \	Merge PR #6648: [tactics] make apply_type safe	Maxime Dénès	2018-02-19
\|\ \
* \ \	Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ...	Maxime Dénès	2018-02-19
\|\ \ \
* \ \ \	Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead.	Maxime Dénès	2018-02-19
\|\ \ \ \
\| \| * \| \|	Change references to CAMLP4 to CAMLP5 to be more accurate since we no	Jim Fehrle	2018-02-17
\| \| \| * \|	apply_type: add option "typecheck" passed down to refine	Enrico Tassi	2018-02-16
\| \|_\|/ / \|/\| \| \|
\| \| \| *	[engine] Remove ghost parameter from `Proofview.Goal.t`	Emilio Jesus Gallego Arias	2018-02-12
\| \|_\|/ \|/\| \|
* \| \|	Merge PR #6651: Use r.(p) syntax to print primitive projections.	Maxime Dénès	2018-02-12
\|\ \ \ \| \|_\|/ \|/\| \|
* \| \|	Merge PR #6686: Kernel/checker reduction cleanups around projection unfolding	Maxime Dénès	2018-02-07
\|\ \ \
* \ \ \	Merge PR #6653: [vernac] Remove VernacGoal, allow anonymous definitions in Ve...	Maxime Dénès	2018-02-05
\|\ \ \ \
\| \| * \| \|	Reductionops.nf_* now take an environment.	Gaëtan Gilbert	2018-02-02
\| \|/ / / \|/\| \| \|
\| * \| \|	[vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinition	Vincent Laporte	2018-02-01
* \| \| \|	Delete duplicate line	Paul Steckler	2018-01-30
\|/ / /
\| * /	Use r.(p) syntax to print primitive projections.	Maxime Dénès	2018-01-30
\|/ /
* \|	Remove dead code from funind.	Maxime Dénès	2018-01-24
* \|	Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder.	Maxime Dénès	2018-01-18
\|\ \
\| * \|	Use let-in aware prod_applist_assum in dtauto and firstorder.	Jasper Hugunin	2018-01-17
* \| \|	Merge PR #6499: [vernac] Move the flags/attributes out of vernac_expr	Maxime Dénès	2018-01-16
\|\ \ \
* \ \ \	Merge PR #6551: Bracket with goal selector	Maxime Dénès	2018-01-16
\|\ \ \ \ \| \|_\|/ / \|/\| \| \|
\| \| * \|	[vernac] vernac_expr no longer recursive	Vincent Laporte	2018-01-08
* \| \| \|	Merge PR #6497: Add optimize_heap tactic for #6488	Maxime Dénès	2018-01-08
\|\ \ \ \ \| \|_\|/ / \|/\| \| \|
\| \| \| *	Remove dir-locals and ship suggested helper hooks instead.	Gaëtan Gilbert	2018-01-06
\| \|_\|/ \|/\| \|
\| \| *	Brackets support single numbered goal selectors.	Théo Zimmermann	2018-01-05
\| \|/ \|/\|
\| *	add optimize_heap tactic for #6488	Paul Steckler	2018-01-03
* \|	Merge PR #6493: [API] remove large file containing duplicate interfaces	Maxime Dénès	2017-12-29
\|\ \
\| * \|	[API] remove large file containing duplicate interfaces	Enrico Tassi	2017-12-27
* \| \|	Remove the local polymorphic flag hack.	Maxime Dénès	2017-12-27
\|/ /
* \|	Merge PR #6439: [api] Also deprecate constructors of Decl_kinds.	Maxime Dénès	2017-12-27
\|\ \
* \ \	Merge PR #6494: Remove legacy Value.normalize function.	Maxime Dénès	2017-12-27
\|\ \ \ \| \|_\|/ \|/\| \|
\| \| *	[api] Also deprecate constructors of Decl_kinds.	Emilio Jesus Gallego Arias	2017-12-23
\| \|/ \|/\|
\| *	Remove legacy Value.normalize function.	Maxime Dénès	2017-12-22
* \|	Separate vernac controls and regular commands.	Maxime Dénès	2017-12-20
\|/
*	Merge PR #6234: Make the micromega extraction check a regular output test.	Maxime Dénès	2017-12-20
\|\
* \	Merge PR #6381: A version of [time] that works on constr evaluation	Maxime Dénès	2017-12-18
\|\ \
* \ \	Merge PR #6406: Make [abstract] nodes show up in the Ltac profile	Maxime Dénès	2017-12-18
\|\ \ \
* \ \ \	Merge PR #6380: Add tactics to reset and display the Ltac profile	Maxime Dénès	2017-12-18
\|\ \ \ \
* \ \ \ \	Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in Extra...	Maxime Dénès	2017-12-18
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6411: Fix #5081 by more fine-grained LtacProf recording	Maxime Dénès	2017-12-18
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6419: [vernac] Split `command.ml` into separate files.	Maxime Dénès	2017-12-18
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.	Maxime Dénès	2017-12-18
\|\ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \|	[flags] Make program_mode a parameter for commands in vernac.	Emilio Jesus Gallego Arias	2017-12-17
\| \| * \| \| \| \| \| \|	[vernac] Split `command.ml` into separate files.	Emilio Jesus Gallego Arias	2017-12-17
\| \|/ / / / / / /
* \| \| \| \| \| \| \|	Merge PR #6219: Document undocumented options	Maxime Dénès	2017-12-15
\|\ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \|	[econstr] Switch constrintern API to non-imperative style.	Emilio Jesus Gallego Arias	2017-12-15
\| \| \| \| \| \| * \| \|	Pass a ghost location for abstract	Jason Gross	2017-12-14
\| \| \| \| \| \| * \| \|	Make [abstract] nodes show up in the Ltac profile	Jason Gross	2017-12-14
\| \|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \|
\| * \| \| \| \| \| \|	Deprecate dead option Match Strict (ssr).	Gaëtan Gilbert	2017-12-14
\| * \| \| \| \| \| \|	Deprecate dead code option Congruence Depth.	Gaëtan Gilbert	2017-12-14
\| \| \| \| \| \| * \|	Add named timers to LtacProf	Jason Gross	2017-12-14
\| \| \| \| \| \|/ /