coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixing coqdoc bug #3292 (unfortunate collision betweens the relative	Hugo Herbelin	2014-04-28
*	Fixing #3293 (eta-expansion at "match" printing time was failing	Hugo Herbelin	2014-04-28
*	Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to	Hugo Herbelin	2014-04-28
*	Rewriting [lapply] tactic in the new monad.	Pierre-Marie Pédrot	2014-04-27
*	Giving true proof-terms in inversion instead of metas.	Pierre-Marie Pédrot	2014-04-27
*	coq_makefile: -I for the new stm/ dir	Enrico Tassi	2014-04-25
*	Adding a stm/ folder, as asked during last workgroup. It was essentially moving	Pierre-Marie Pédrot	2014-04-25
*	Removing Autoinstance once and for all.	Pierre-Marie Pédrot	2014-04-25
*	Removing useless try-with clauses in Goal.enter variants.	Pierre-Marie Pédrot	2014-04-25
*	Future: memory optimization when forcing a chained pure computation	Enrico Tassi	2014-04-25
*	Opaqueproofs: sink futures when interactive	Enrico Tassi	2014-04-25
*	print futures in caml toplevel too	Enrico Tassi	2014-04-25
*	Fix a second, trickier, typo in Termops.eta_reduce_head.	Arnaud Spiwack	2014-04-25
*	Adding a debug printer for futures.	Pierre-Marie Pédrot	2014-04-25
*	Fixing various backtrace recordings.	Pierre-Marie Pédrot	2014-04-25
*	Fix a small typo in Termops.eta_reduce_head.	Arnaud Spiwack	2014-04-25
*	Adding a [fold_map] operation on constrs.	Pierre-Marie Pédrot	2014-04-24
*	Writing tclABSTRACT in the new monad. In particular the unsafe status is now	Pierre-Marie Pédrot	2014-04-24
*	Better representation of evar filters: we represent the vacuous filters of	Pierre-Marie Pédrot	2014-04-23
*	Removing dead code, thanks to new OCaml warnings and a bit of scripting.	Pierre-Marie Pédrot	2014-04-23
*	Import proof of decidability of negated formulas from Coquelicot.	Guillaume Melquiond	2014-04-23
*	Remove some uses of excluded middle.	Guillaume Melquiond	2014-04-22
*	Replace the proof of sig_forall_dec from Kaliszyk/O'Connor by the one from Co...	Guillaume Melquiond	2014-04-22
*	Add regression tests for 3188 and 3265	Jason Gross	2014-04-22
*	Removing the compatibility layer from Leminv. Also removed an undocumented	Pierre-Marie Pédrot	2014-04-22
*	Using the new monad tactic in Inv.	Pierre-Marie Pédrot	2014-04-22
*	Removing tactic compatibility layer from Elim.	Pierre-Marie Pédrot	2014-04-22
*	Small code cleaning in Tacticals.	Pierre-Marie Pédrot	2014-04-22
*	Simplifying interface of elimination tactics. They used dummy clausenvs, and	Pierre-Marie Pédrot	2014-04-22
*	Adding a test for bug #2923.	Pierre-Marie Pédrot	2014-04-20
*	Adding a test for bug #3285.	Pierre-Marie Pédrot	2014-04-20
*	Fixing bug #3285.	Pierre-Marie Pédrot	2014-04-20
*	Adding a [map] primitive to the tactic monad. Hopefully this should be	Pierre-Marie Pédrot	2014-04-20
*	Fixing missing headers.	Hugo Herbelin	2014-04-16
*	Closing bug #3260	Julien Forest	2014-04-14
*	Fix guard condition for nested cofixpoints in checker.	Maxime Dénès	2014-04-10
*	Fix guard condition for nested cofixpoints.	Maxime Dénès	2014-04-10
*	better description of bug 3251	Enrico Tassi	2014-04-10
*	Have the feedback bus as a backend for dumping globs.	Carst Tankink	2014-04-10
*	Dumpglob: factor out reference dumping.	Carst Tankink	2014-04-10
*	CoqIDE: options for syntax highlighting	Enrico Tassi	2014-04-10
*	CoqIDE: removing a timer may raise an exception	Enrico Tassi	2014-04-10
*	coqtop -batch refuses Back 1 but accepts Undo.	Pierre Boutillier	2014-04-10
*	By resolution of the CoqWG, instantiate must not be used now that refine works	Pierre Boutillier	2014-04-10
*	No more Coersion in Init.	Pierre Boutillier	2014-04-10
*	Define [projT3] and [proj3_sig]	Jason Gross	2014-04-10
*	Test case for bug 3037	Jason Gross	2014-04-10
*	Test case for 3164	Jason Gross	2014-04-10
*	Test case for bug 3262	Jason Gross	2014-04-10
*	Test case for bug #3217	Jason Gross	2014-04-10