coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Cleaning of the new implementation of the tactic monad.	Arnaud Spiwack	2014-08-04
*	A tentative uniform naming policy in module Inductiveops.	Hugo Herbelin	2014-08-01
*	Removing more tactic compatibility layer.	Pierre-Marie Pédrot	2014-08-01
*	Removing some tactic compatibility layer.	Pierre-Marie Pédrot	2014-08-01
*	Add an option to solve typeclass goals generated by apply which can't be	Matthieu Sozeau	2014-07-31
*	Restore proper order of effects in letin_tac_gen. Fixes CFGV again.	Matthieu Sozeau	2014-07-03
*	Synchronized names from the "as" clause with the skeleton of the	Hugo Herbelin	2014-06-30
*	Small refinement about whether it is tolerated for compatibility that	Hugo Herbelin	2014-06-28
*	Moved code for finding subterms (pattern, induction, set, generalize, ...)	Hugo Herbelin	2014-06-28
*	Extra check for indirect dependency when abstracting a term which is	Hugo Herbelin	2014-06-28
*	Made the subterm finding function make_abstraction independent of the	Hugo Herbelin	2014-06-28
*	Incorrect folding of evars in let_tac_gen made remember fail to store	Matthieu Sozeau	2014-06-25
*	In exact check, use e_type_of to ensure that universe constraints necessary	Matthieu Sozeau	2014-06-25
*	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
*	Removing opens to Clenvtac to track its use more easily.	Pierre-Marie Pédrot	2014-06-23
*	Fix semantics of change p with c to typecheck c at each specific occurrence o...	Matthieu Sozeau	2014-06-23
*	Proofs now take and return an evar_universe_context, simplifying interfaces	Matthieu Sozeau	2014-06-18
*	Check resolution of Metas turned into Evars by pose_all_metas_as_evars	Hugo Herbelin	2014-06-13
*	Passing some tactics to the new monad type.	Pierre-Marie Pédrot	2014-06-12
*	fix handling of side effects in abstract (fixes QArithSternBrocot)	Enrico Tassi	2014-06-11
*	Preserve compatibility on examples such as "intros []." on goals such	Hugo Herbelin	2014-06-06
*	Collecting in Namegen those conventional default names that are used in diffe...	Hugo Herbelin	2014-06-04
*	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
*	- Fix in kernel conversion not folding the universe constraints	Matthieu Sozeau	2014-05-26
*	Moving the "specialize" tactic out of the AST. Also removed an obsolete	Pierre-Marie Pédrot	2014-05-22
*	Code cleaning & factorizing functions in Equality.	Pierre-Marie Pédrot	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
*	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
*	Use new tactic combinators in tclABSTRACT, to avoid blowup when using V82.tac...	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 eq_constr_universes restricted to Sorts.equal	Matthieu Sozeau	2014-05-06
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	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
*	Better hashconsing of levels and universes, working with modules.	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Rewriting [lapply] tactic in the new monad.	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
*	Removing tactic compatibility layer from Elim.	Pierre-Marie Pédrot	2014-04-22
*	Closing bug #3164	Julien Forest	2014-04-04