coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Removing dead code relative to or_metaid.	Pierre-Marie Pédrot	2014-07-25
*	CHANGES: cycle and swap.	Arnaud Spiwack	2014-07-25
*	Document swap tactic.	Arnaud Spiwack	2014-07-25
*	Document cycle tactic.	Arnaud Spiwack	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
*	A slightly more fine grained way to check whether a TACTIC EXTEND is global o...	Arnaud Spiwack	2014-07-25
*	CHANGES: yellow in Coqide.	Arnaud Spiwack	2014-07-25
*	CHANGE: add Derive.	Arnaud Spiwack	2014-07-25
*	CHANGE: document the features of the new tactic engine.	Arnaud Spiwack	2014-07-25
*	Update the documentation of Ltac's ";" and ";[…]" to reflect the new multi-...	Arnaud Spiwack	2014-07-25
*	Warns about inconsistency of generated name in evars and goals.	Arnaud Spiwack	2014-07-25
*	- Do module substitution inside mind_record.	Matthieu Sozeau	2014-07-25
*	More documentation of universes.	Matthieu Sozeau	2014-07-25
*	Add emacs auto-save and crash-save files to the .gitignore.	Arnaud Spiwack	2014-07-25
*	Add *.crashcoqide files to the .gitignore.	Arnaud Spiwack	2014-07-25
*	Add lia.cache to the .gitignore	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
*	Forgot to add a Universes.v.tex as a target.	Matthieu Sozeau	2014-07-24
*	Start documenting universe polymorphism.	Matthieu Sozeau	2014-07-24
*	Distinguish tactics t1;t2 and t1;[t2..].	Arnaud Spiwack	2014-07-24
*	A handful of useful primitives in Proofview.Refine.	Arnaud Spiwack	2014-07-24
*	Fix misleading pretty-printing of information for non-universe-polymorphic	Matthieu Sozeau	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
*	Revert "Adding a "is_val" primitive to IStream."	Pierre-Marie Pédrot	2014-07-24
*	fixup fakeide test-suite	Pierre Boutillier	2014-07-24
*	Make MacStore like coqide more	Pierre Boutillier	2014-07-24
*	Derive plugin: document new syntax.	Arnaud Spiwack	2014-07-23
*	Derive plugin: add some comments.	Arnaud Spiwack	2014-07-23
*	Derive plugin: code reorganisation for clarity.	Arnaud Spiwack	2014-07-23
*	Derive plugin: small refactoring.	Arnaud Spiwack	2014-07-23
*	Derive plugin: a more general interface.	Arnaud Spiwack	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-23
*	Porting guard fix to checker.	Maxime Dénès	2014-07-22
*	Minor cleaning.	Maxime Dénès	2014-07-22
*	Revert "Extend subterm relation to pattern matching in return predicates."	Maxime Dénès	2014-07-22
*	Revert "Propagate size info through pattern matching in predicates, for the"	Maxime Dénès	2014-07-22
*	Propagate size info through pattern matching in predicates, for the	Maxime Dénès	2014-07-22
*	Extend subterm relation to pattern matching in return predicates.	Maxime Dénès	2014-07-22
*	Fix check_inductive_codomain.	Maxime Dénès	2014-07-22
*	Refine check_is_subterm.	Maxime Dénès	2014-07-22
*	Refined guard condition of cofixpoints, to anticipate potential futur	Maxime Dénès	2014-07-22
*	First attempt at a fix for guard condition on cofixpoints.	Maxime Dénès	2014-07-22
*	Add test-suite file for guard condition on cofixpoints.	Maxime Dénès	2014-07-22