coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Better structure for Ltac pretyping environments.	Pierre-Marie Pédrot	2014-08-07
*	Hypotheses in [Proofview.Goal.enter] were not normalised.	Arnaud Spiwack	2014-08-07
*	[uconstr]: use a closure instead of eager substitution.	Arnaud Spiwack	2014-08-06
*	Adding a [make] primitive to the NonLogical monad.	Pierre-Marie Pédrot	2014-08-05
*	Uncountably many bullets (+,-,,++,--,*,+++,...).	Hugo Herbelin	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-05
*	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-04
*	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