coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Small optimization in clear_body.	Pierre-Marie Pédrot	2016-06-20
*	Adding an "as" clause to specialize.	Hugo Herbelin	2016-06-18
*	Giving a more natural semantics to injection by default.	Hugo Herbelin	2016-06-18
*	Exporting a generic argument induction_arg. As a consequence,	Hugo Herbelin	2016-06-18
*	A cleaning phase around delayed induction arg + exporting force_induction_arg.	Hugo Herbelin	2016-06-18
*	Adding eintros to respect the e- prefix policy.	Hugo Herbelin	2016-06-18
*	Typeclasses:rename solve_instantiation* & use Hook	Matthieu Sozeau	2016-06-16
*	Fix resolve_one_typeclass to use the new engine	Matthieu Sozeau	2016-06-16
*	Bind resolve_one_typeclass to 8.5 or 8.6 resolution	Matthieu Sozeau	2016-06-16
*	Put autoapply back, lost during rebase	Matthieu Sozeau	2016-06-16
*	Cleanup and refactoring	Matthieu Sozeau	2016-06-16
*	Extend Hint Mode to handle the no-head-evar case	Matthieu Sozeau	2016-06-16
*	Revise syntax of Hint Cut	Matthieu Sozeau	2016-06-16
*	Purely refactoring and code/API cleanup.	Matthieu Sozeau	2016-06-16
*	bteauto: a Proofview.tactic for multiple goals	Matthieu Sozeau	2016-06-16
*	Typeclasses: allow shelved subgoals	Matthieu Sozeau	2016-06-16
*	Minor cleanup	Matthieu Sozeau	2016-06-16
*	Typeclasses: refine the eauto tactic	Matthieu Sozeau	2016-06-16
*	Typeclasses: verbosity and Limit Intros options	Matthieu Sozeau	2016-06-16
*	typeclass resolution: add two compatibility options	Matthieu Sozeau	2016-06-16
*	Fix incorrect caching of local hints w.r.t sections	Matthieu Sozeau	2016-06-16
*	Compat with ocaml 4.01	Matthieu Sozeau	2016-06-16
*	Fix iterative deepening strategy failing too early	Matthieu Sozeau	2016-06-16
*	Implement limited proof search and iterative deepening.	Matthieu Sozeau	2016-06-16
*	Typeclasses eauto based on new proof engine,	Matthieu Sozeau	2016-06-16
*	A stronger invariant on the syntax of TacAssert, what allows for a	Hugo Herbelin	2016-06-16
*	Merge 'pr/191' into trunk	Enrico Tassi	2016-06-16
\|\
* \	Merge PR #100: fresh now accepts more things than just identifiers.	Pierre-Marie Pédrot	2016-06-16
\|\ \
\| \| *	Goal selectors are now tacticals and can be used as such.	Cyprien Mangin	2016-06-14
\| \|/ \|/\|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-13
\|\ \
\| * \|	Fixing a try with in apply that has become too weak in 8.5.	Hugo Herbelin	2016-06-11
* \| \|	Adding a bit of documentation in the mli.	Pierre-Marie Pédrot	2016-06-09
\| * \|	Improve the interpretation scope of arguments of an ltac match.	Hugo Herbelin	2016-06-09
* \| \|	Fixing #4787 (Unset Bracketing Last Introduction Pattern not working).	Hugo Herbelin	2016-06-07
* \| \|	Removing the Q_constr file.	Pierre-Marie Pédrot	2016-06-05
* \| \|	Moving Hipattern to a regular ML file.	Pierre-Marie Pédrot	2016-06-05
* \| \|	Removing PATTERN uses in Hipattern.	Pierre-Marie Pédrot	2016-06-05
* \| \|	Add a synonymous Set Debug Typeclasses for Set Typeclasses Debug, for uniform...	Hugo Herbelin	2016-06-02
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-01
\|\\| \|
\| * \|	Revert "Rename Lexer -> CLexer."	Pierre-Marie Pédrot	2016-05-31
* \| \|	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
\| * \|	Fix bug #4746: Anomaly: Evar ?X10 was not declared.	Pierre-Marie Pédrot	2016-05-29
\| * \|	rewrite/Univs: Fix bug # 4498.	Matthieu Sozeau	2016-05-26
\| * \|	Hints/Univs: fix bug #4628 anomalies	Matthieu Sozeau	2016-05-23
* \| \|	Removing some compatibility layers in Tactics.	Pierre-Marie Pédrot	2016-05-17
* \| \|	Removing the old refine tactic from the Tactics module.	Pierre-Marie Pédrot	2016-05-17
* \| \|	Put the "move" tactic in the monad.	Pierre-Marie Pédrot	2016-05-17
* \| \|	Put the "change" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
* \| \|	Put the "specialize_eq" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
* \| \|	Put the "generalize dependent" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16