coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #6960: [api] Move some types to their proper module.	Pierre-Marie Pédrot	2018-04-06
\|\
* \|	Fix #6404 - Print tactics called by ML tactics	Jason Gross	2018-04-02
\| *	[api] Move some types to their proper module.	Emilio Jesus Gallego Arias	2018-04-02
\|/
*	[ssreflect] Fix module scoping problems due to packing and mli files.	Emilio Jesus Gallego Arias	2018-03-10
*	[located] Push inner locations in `reference` to a CAst.t node.	Emilio Jesus Gallego Arias	2018-03-09
*	[located] More work towards using CAst.t	Emilio Jesus Gallego Arias	2018-03-09
*	Allow using cumulativity without forcing strict constraints.	Gaëtan Gilbert	2018-03-09
*	Merge PR #6496: Generate typed generic code from ltac macros	Maxime Dénès	2018-03-09
\|\
\| *	Make most of TACTIC EXTEND macros runtime calls.	Maxime Dénès	2018-03-08
* \|	Rename some universe minimizing "normalize" functions to "minimize"	Gaëtan Gilbert	2018-03-06
\|/
*	Merge PR #6898: [compat] Remove "Intuition Iff Unfolding"	Maxime Dénès	2018-03-06
\|\
* \	Merge PR #6855: Update headers following #6543.	Maxime Dénès	2018-03-05
\|\ \
* \ \	Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.	Maxime Dénès	2018-03-04
\|\ \ \
* \ \ \	Merge PR #6846: Moving code for "simple induction"/"simple destruct" to coret...	Maxime Dénès	2018-03-04
\|\ \ \ \
* \ \ \ \	Merge PR #6676: [proofview] goals come with a state	Maxime Dénès	2018-03-04
\|\ \ \ \ \
\| \| \| \| \| *	[compat] Remove "Intuition Iff Unfolding"	Emilio Jesus Gallego Arias	2018-03-03
\| \|_\|_\|_\|/ \|/\| \| \| \|
\| \| * \| \|	Moving code for "simple induction"/"simple destruct" to coretactics.ml4.	Hugo Herbelin	2018-03-01
\| \|/ / / \|/\| \| \|
\| \| * \|	[econstr] Continue consolidation of EConstr API under `interp`.	Emilio Jesus Gallego Arias	2018-02-28
\| \|/ / \|/\| \|
\| \| *	Update headers following #6543.	Théo Zimmermann	2018-02-27
\| \|/ \|/\|
* \|	[ast] Improve precision of Ast location recognition in serialization.	Emilio Jesus Gallego Arias	2018-02-22
\| *	proofview: goals come with a state	Enrico Tassi	2018-02-20
* \|	Moving Metasyntax.register_grammar to Pcoq for usability in Egramcoq.	Hugo Herbelin	2018-02-20
* \|	Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.	Hugo Herbelin	2018-02-20
\|/
*	Change references to CAMLP4 to CAMLP5 to be more accurate since we no	Jim Fehrle	2018-02-17
*	Reductionops.nf_* now take an environment.	Gaëtan Gilbert	2018-02-02
*	Merge PR #6551: Bracket with goal selector	Maxime Dénès	2018-01-16
\|\
* \	Merge PR #6497: Add optimize_heap tactic for #6488	Maxime Dénès	2018-01-08
\|\ \
\| \| *	Brackets support single numbered goal selectors.	Théo Zimmermann	2018-01-05
\| \|/ \|/\|
\| *	add optimize_heap tactic for #6488	Paul Steckler	2018-01-03
* \|	Remove the local polymorphic flag hack.	Maxime Dénès	2017-12-27
* \|	Remove legacy Value.normalize function.	Maxime Dénès	2017-12-22
\|/
*	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 #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
\|\ \ \ \ \
\| * \| \| \| \|	[flags] Make program_mode a parameter for commands in vernac.	Emilio Jesus Gallego Arias	2017-12-17
\| \| \| \| * \|	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
\| \|_\|_\|/ / \|/\| \| \| \|
\| \| \| \| *	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 #6379: Fix profiling plugin	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
\| \| \| \| \| \|/
\| \| \| * \| \|	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
\| \|_\|/ \|/\| \|