coq - The formal proof system

Age	Commit message (Expand)	Author
2014-08-05	A new step in the new "standard" naming policy for propositional hypotheses	Hugo Herbelin
2014-08-05	STM: new "par:" goal selector, like "all:" but in parallel	Enrico Tassi
2014-08-05	Goal: API to get the solution of a goal	Enrico Tassi
2014-08-05	Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter].	Arnaud Spiwack
2014-08-04	Some comments in the interface of Proofview_monad.	Arnaud Spiwack
2014-08-04	Cleaning the new implementation of the tactic monad continued.	Arnaud Spiwack
2014-08-04	Cleaning of the new implementation of the tactic monad.	Arnaud Spiwack
2014-08-01	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-07-31	Making the error message about bullets more precise.	Pierre Courtieu
2014-07-28	Adding a tclBREAK primitive to the tactic monad.	Pierre-Marie Pédrot
2014-07-25	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-24	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-23	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-14	Adding a delay to tclTIME.	Pierre-Marie Pédrot
2014-07-13	Adding a "time" tactical for benchmarking purposes. In case the tactic	Hugo Herbelin
2014-07-11	Feedback: LoadedFile + Goals	Enrico Tassi
2014-07-10	check_for_interrupt: better (but slower) in threading mode	Enrico Tassi
2014-07-08	Exporting Proof.split in proofview.	Pierre-Marie Pédrot
2014-07-07	Revert "time tac" (committed by mistake).	Hugo Herbelin
2014-07-07	time tac	Hugo Herbelin
2014-06-25	Putting implicit arguments of Clenv.res_pf right.	Pierre-Marie Pédrot
2014-06-24	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-23	Clenvtac.unify is in the new monad.	Pierre-Marie Pédrot
2014-06-19	Adding a raw_goals primitive for Tacinterp.	Pierre-Marie Pédrot
2014-06-18	Proofs now take and return an evar_universe_context, simplifying interfaces	Matthieu Sozeau
2014-06-17	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-13	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-10	Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...	Matthieu Sozeau
2014-06-07	Adding a new Control file centralizing the control options of Coq.	Pierre-Marie Pédrot
2014-06-04	Collecting in Namegen those conventional default names that are used in diffe...	Hugo Herbelin
2014-06-03	The tactic interpreter now uses a new type of tactics, through	Pierre-Marie Pédrot
2014-06-01	Use of "H"-based names for propositional hypotheses obtained by	Hugo Herbelin
2014-05-26	- Fix in kernel conversion not folding the universe constraints	Matthieu Sozeau
2014-05-24	Revert "Chasing the goal entering backward while interpreting tactics. This r...	Pierre-Marie Pédrot