coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Removing useless use of metaids in tactic AST.	Pierre-Marie Pédrot	2014-05-22
*	Removing decompose record / sum from the tactic AST.	Pierre-Marie Pédrot	2014-05-21
*	Allowing Ltac definitions that may be unusable because of a built-in	Pierre-Marie Pédrot	2014-05-21
*	Moving left & right tactics out of the AST.	Pierre-Marie Pédrot	2014-05-21
*	Moving (e)transitivity out of the AST.	Pierre-Marie Pédrot	2014-05-20
*	Tactics declared through TACTIC EXTEND that are of the form	Pierre-Marie Pédrot	2014-05-20
*	Tentative to add constr-using primitive tactics without grammar rules.	Pierre-Marie Pédrot	2014-05-20
*	When discrimination is not possible, try to project.	Maxime Dénès	2014-05-18
*	Suggest Set Injection On Proofs in error message for injection.	Maxime Dénès	2014-05-18
*	Restored old behavior of injection on proofs by default.	Maxime Dénès	2014-05-18
*	Moving argument-free tactics out of the AST into a dedicated	Pierre-Marie Pédrot	2014-05-16
*	poly: remove unused attribute to STM nodes and vernac classificaiton	Enrico Tassi	2014-05-15
*	Now parsing rules of ML-declared tactics are only made available after the	Pierre-Marie Pédrot	2014-05-12
*	Code cleaning & factorizing functions in Equality.	Pierre-Marie Pédrot	2014-05-09
*	Update and start testing rewrite-in-type code.	Matthieu Sozeau	2014-05-09
*	Refresh universes for Ltac's type_of, as the term can be used anywhere,	Matthieu Sozeau	2014-05-09
*	Encapsulating some clausenv uses. This simplifies the control flow of some	Pierre-Marie Pédrot	2014-05-08
*	Revert "Avoid "revert" to retype-check the goal, and move it to a "new" tactic."	Hugo Herbelin	2014-05-08
*	Avoid "revert" to retype-check the goal, and move it to a "new" tactic.	Hugo Herbelin	2014-05-08
*	Isolating a function "make_abstraction", new name of "letin_abstract",	Hugo Herbelin	2014-05-08
*	Simplification and improvement of "subst x" in such a way that it	Hugo Herbelin	2014-05-08
*	Renaming new_induct -> induction; new_destruct -> destruct.	Hugo Herbelin	2014-05-08
*	Little reorganization of generalize tactics code w/o semantic changes.	Hugo Herbelin	2014-05-08
*	- Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ...	Matthieu Sozeau	2014-05-08
*	Moving Dnet-related code to tactics/.	Pierre-Marie Pédrot	2014-05-08
*	Code cleaning in Tacinterp: factorizing some uses of tclEVARS.	Pierre-Marie Pédrot	2014-05-08
*	Cleanup before merge with the trunk	Matthieu Sozeau	2014-05-06
*	Use new tactic combinators in tclABSTRACT, to avoid blowup when using V82.tac...	Matthieu Sozeau	2014-05-06
*	- Fix treatment of global universe constraints which should be passed along	Matthieu Sozeau	2014-05-06
*	Avoid u+k <= v constraints, don't take the sup of an algebraic universe during	Matthieu Sozeau	2014-05-06
*	- Fix arity handling in retyping (de Bruijn bug!)	Matthieu Sozeau	2014-05-06
*	- Fix eq_constr_universes restricted to Sorts.equal	Matthieu Sozeau	2014-05-06
*	Fixes after rebase. The use of pf_constr_of_global is problematic in presence...	Matthieu Sozeau	2014-05-06
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	2014-05-06
*	Adapt Y. Bertot's path on private inductives (now the keyword is "Private").	Yves Bertot	2014-05-06
*	- Fix abstract forgetting about new constraints.	Matthieu Sozeau	2014-05-06
*	- Fix handling of polymorphic inductive elimination schemes.	Matthieu Sozeau	2014-05-06
*	Various fixes of universe polymorphism and projections when they're set.	Matthieu Sozeau	2014-05-06
*	Better hashconsing of levels and universes, working with modules.	Matthieu Sozeau	2014-05-06
*	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau	2014-05-06
*	Rework handling of universes on top of the STM, allowing for delayed	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Trying to improve the error messages of injection.	Maxime Dénès	2014-04-30
*	Injection: do not fail when arguments have sort Prop.	Maxime Dénès	2014-04-29
*	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
*	Removing useless try-with clauses in Goal.enter variants.	Pierre-Marie Pédrot	2014-04-25
*	Fixing various backtrace recordings.	Pierre-Marie Pédrot	2014-04-25
*	Writing tclABSTRACT in the new monad. In particular the unsafe status is now	Pierre-Marie Pédrot	2014-04-24
*	Removing dead code, thanks to new OCaml warnings and a bit of scripting.	Pierre-Marie Pédrot	2014-04-23