coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[vernac] vernac_expr no longer recursive	Vincent Laporte	2018-01-08
*	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
\| \| \| \| \| \|/ /
\| \| \| \| \| * /	Add tactics to reset and display the Ltac profile	Jason Gross	2017-12-14
\| \|_\|_\|_\|/ / \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR #6386: Catch errors while coercing 'and' intro patterns	Maxime Dénès	2017-12-14
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6116: ssr: fill_occ_pattern: return valid ustate even if no match (...	Maxime Dénès	2017-12-14
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6379: Fix profiling plugin	Maxime Dénès	2017-12-14
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #978: In printing, experimenting factorizing "match" clauses with sa...	Maxime Dénès	2017-12-14
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #6169: Clean up/deprecated options	Maxime Dénès	2017-12-14
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.	Maxime Dénès	2017-12-14
\|\ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| * \| \|	Fix #5081 by more fine-grained LtacProf recording	Jason Gross	2017-12-12
\| \| \| \| \| \| \| \| \|/ / /
\| \| \| * \| \| \| \| \| \| \|	In printing, factorizing "match" clauses with same right-hand side.	Hugo Herbelin	2017-12-12
\| \| \| * \| \| \| \| \| \| \|	Removing cumbersome location in multiple patterns.	Hugo Herbelin	2017-12-12
\| \| \| \| * \| \| \| \| \| \|	Use msg_info for LtacProf	Jason Gross	2017-12-11
\| \| \| \| * \| \| \| \| \| \|	Allow LtacProf tactics to be called	Jason Gross	2017-12-11
\| \| \| \| \| \|_\|_\|/ / / \| \| \| \| \|/\| \| \| \| \|
\| \| \| \| \| \| * \| \| \|	Catch errors while coercing 'and' intro patterns	Tej Chajed	2017-12-11
\| \| \| \| \| \|/ / / / \| \| \| \| \|/\| \| \| \|
* \| \| \| / \| \| \| \|	[proof] Embed evar_map in RefinerError exception.	Emilio Jesus Gallego Arias	2017-12-11
\| \|_\|_\|/ / / / / \|/\| \| \| \| \| \| \|
\| \| * \| \| \| \| \|	Remove deprecated appcontext and corresponding documentation.	Théo Zimmermann	2017-12-11
\| \| * \| \| \| \| \|	Remove deprecated option Tactic Compat Context.	Théo Zimmermann	2017-12-11
\| \|/ / / / / / \|/\| \| \| \| \| \|
* \| \| \| \| \| \|	Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract.	Maxime Dénès	2017-12-11
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #1150: [stm] Remove all but one use of VtUnknown.	Maxime Dénès	2017-12-11
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #6338: Remove up-to-conversion term matching	Maxime Dénès	2017-12-11
\|\ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \|	[lib] Rename Profile to CProfile	Emilio Jesus Gallego Arias	2017-12-09
\| \|_\|_\|/ / / / / \|/\| \| \| \| \| \| \|
\| \| * \| \| \| \| \|	[stm] Remove all but one use of VtUnknown.	Emilio Jesus Gallego Arias	2017-12-09
\| \|/ / / / / / \|/\| \| \| \| \| \|
* \| \| \| \| \| \|	Merge PR #6158: Allows a level in the raw and glob printers	Maxime Dénès	2017-12-08
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6322: Fix #6286 (non stability of micromega csdp cache rebuilding)	Maxime Dénès	2017-12-07
\|\ \ \ \ \ \ \ \
\| \| \| * \| \| \| \| \|	Getting rid of pf_is_matching in Funind.	Pierre-Marie Pédrot	2017-12-06
\| \|_\|/ / / / / / \|/\| \| \| \| \| \| \|