coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Collecting in Namegen those conventional default names that are used in diffe...	Hugo Herbelin	2014-06-04
*	- Fix hashing of levels to get the "right" order in universe contexts etc...	Matthieu Sozeau	2014-06-04
*	The tactic interpreter now uses a new type of tactics, through	Pierre-Marie Pédrot	2014-06-03
*	Removing symmetry from the atomic tactics.	Pierre-Marie Pédrot	2014-06-02
*	More on injection over a projectable "existT". - Fixing syntax "injection ......	Hugo Herbelin	2014-05-31
*	Fixing introduction patterns * and ** when used in a branch so that they do n...	Hugo Herbelin	2014-05-31
*	Upgrade Matthieu's new_revert as the "revert" (a "unit tactic").	Hugo Herbelin	2014-05-31
*	Removing a tclSENSITIVE from rewrite.	Pierre-Marie Pédrot	2014-05-27
*	- 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
*	Moving the "specialize" tactic out of the AST. Also removed an obsolete	Pierre-Marie Pédrot	2014-05-22
*	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