coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Add primtive [num_goal] to Proofview.	Arnaud Spiwack	2014-08-01
*	Clean outdated comment in Proofview.Notations.	Arnaud Spiwack	2014-08-01
*	Removing more tactic compatibility layer.	Pierre-Marie Pédrot	2014-08-01
*	Making the error message about bullets more precise.	Pierre Courtieu	2014-07-31
*	Adding a tclBREAK primitive to the tactic monad.	Pierre-Marie Pédrot	2014-07-28
*	Add a tactic [swap i j] to swap the position of goals [i] and [j].	Arnaud Spiwack	2014-07-25
*	Adds a cycle tactic to reorder goals in a loop.	Arnaud Spiwack	2014-07-25
*	Small reorganisation in proof.ml.	Arnaud Spiwack	2014-07-25
*	Fail gracefully when focusing on non-existing goals with user commands.	Arnaud Spiwack	2014-07-25
*	Fix handling of universes at the end of proofs, esp. for async proof processing.	Matthieu Sozeau	2014-07-25
*	A handful of useful primitives in Proofview.Refine.	Arnaud Spiwack	2014-07-24
*	Adding a tail-rec tclONCE.	Pierre-Marie Pédrot	2014-07-24
*	New implementation of the tactic monad.	Pierre-Marie Pédrot	2014-07-24
*	When closing a proof, make sure that the types have their evar substituted.	Arnaud Spiwack	2014-07-23
*	Proof_global: an unused variable replaced by a wildcard.	Arnaud Spiwack	2014-07-23
*	Proof_global.start_dependent_proof: properly threads the sigma through the te...	Arnaud Spiwack	2014-07-23
*	Change the interface of proof_global to take an evar_map instead of a univers...	Arnaud Spiwack	2014-07-23
*	Adding a delay to tclTIME.	Pierre-Marie Pédrot	2014-07-14
*	Adding a "time" tactical for benchmarking purposes. In case the tactic	Hugo Herbelin	2014-07-13
*	Feedback: LoadedFile + Goals	Enrico Tassi	2014-07-11
*	check_for_interrupt: better (but slower) in threading mode	Enrico Tassi	2014-07-10
*	Exporting Proof.split in proofview.	Pierre-Marie Pédrot	2014-07-08
*	Revert "time tac" (committed by mistake).	Hugo Herbelin	2014-07-07
*	time tac	Hugo Herbelin	2014-07-07
*	Putting implicit arguments of Clenv.res_pf right.	Pierre-Marie Pédrot	2014-06-25
*	Force the final universe context of a proof only in poly \|\| now case.	Matthieu Sozeau	2014-06-24
*	Clenvtac.clenv_refine in the new monad. Not satisfactory though, because it	Pierre-Marie Pédrot	2014-06-24
*	Clenvtac.res_pf is in the new tactic monad.	Pierre-Marie Pédrot	2014-06-24
*	Clenvtac.unify is in the new monad.	Pierre-Marie Pédrot	2014-06-23
*	Adding a raw_goals primitive for Tacinterp.	Pierre-Marie Pédrot	2014-06-19
*	Proofs now take and return an evar_universe_context, simplifying interfaces	Matthieu Sozeau	2014-06-18
*	Tentative optimization not to nf_evar too often in the compatibility	Pierre-Marie Pédrot	2014-06-17
*	Removing dead code.	Pierre-Marie Pédrot	2014-06-17
*	Safer entry point of primitive projections in the kernel, now it does recognize	Matthieu Sozeau	2014-06-17
*	Improving tclWITHHOLES which did not see undefined evars up to	Hugo Herbelin	2014-06-13
*	Fixing "clear" in internal_cut_replace: forbid dependencies in the	Hugo Herbelin	2014-06-13
*	Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...	Matthieu Sozeau	2014-06-10
*	Adding a new Control file centralizing the control options of Coq.	Pierre-Marie Pédrot	2014-06-07
*	Collecting in Namegen those conventional default names that are used in diffe...	Hugo Herbelin	2014-06-04
*	The tactic interpreter now uses a new type of tactics, through	Pierre-Marie Pédrot	2014-06-03
*	Use of "H"-based names for propositional hypotheses obtained by	Hugo Herbelin	2014-06-01
*	- Fix in kernel conversion not folding the universe constraints	Matthieu Sozeau	2014-05-26
*	Revert "Chasing the goal entering backward while interpreting tactics. This r...	Pierre-Marie Pédrot	2014-05-24
*	Chasing the goal entering backward while interpreting tactics. This required	Pierre-Marie Pédrot	2014-05-24
*	Another try at close_proof that should behave better w.r.t. exception handling.	Matthieu Sozeau	2014-05-16
*	- Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ...	Matthieu Sozeau	2014-05-08
*	- Fix treatment of global universe constraints which should be passed along	Matthieu Sozeau	2014-05-06
*	Fix set_leq_sort refusing max(u,Set) <= Set when u is flexible.	Matthieu Sozeau	2014-05-06
*	- Fixes for canonical structure resolution (check that the initial term indee...	Matthieu Sozeau	2014-05-06
*	- Fix eq_constr_universes restricted to Sorts.equal	Matthieu Sozeau	2014-05-06