coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \| \|	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
\| \| \| *	Univs/(e)auto: fix bug #4450 polymorphic exact hints	Matthieu Sozeau	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
* \| \|	Put the "generalize" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
* \| \|	Put the "cofix" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
* \| \|	Put the "*_cast_no_check" tactics in the monad.	Pierre-Marie Pédrot	2016-05-16
* \| \|	Put the "exact" family of tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
* \| \|	Put the "fix" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
* \| \|	Put the "exact_constr" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
* \| \|	Put the "clear" tactic into the monad.	Pierre-Marie Pédrot	2016-05-16
\| * \|	Rename Lexer -> CLexer.	Pierre-Marie Pédrot	2016-05-09
* \| \|	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
* \| \|	Normalizing the names of dynamic types to follow a typ_* scheme.	Pierre-Marie Pédrot	2016-05-04
* \| \|	Removing external uses of Val.inject and making Geninterp.interp return Val.t	Pierre-Marie Pédrot	2016-05-04
* \| \|	Removing the Value.of_* API for parameterized types.	Pierre-Marie Pédrot	2016-05-04
* \| \|	Moving the Val module to Geninterp.	Pierre-Marie Pédrot	2016-05-04
* \| \|	Getting rid of the Geninterp.generic_interp function.	Pierre-Marie Pédrot	2016-05-04
* \| \|	Switching to an untyped toplevel representation for Ltac values.	Pierre-Marie Pédrot	2016-05-04
* \| \|	Moving Ftactic and Geninterp to the engine folder.	Pierre-Marie Pédrot	2016-05-04
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-04
\|\\| \|
\| * \|	In Regular Subst Tactic mode, ensure that the order of hypotheses is	Hugo Herbelin	2016-05-03
\| * \|	Fix bug #4707: clearbody much slower in 8.5pl1.	Pierre-Marie Pédrot	2016-05-03
* \| \|	Revert "In the short term, stronger invariant on the syntax of TacAssert, what"	Hugo Herbelin	2016-04-27
* \| \|	In the short term, stronger invariant on the syntax of TacAssert, what	Hugo Herbelin	2016-04-27
\| \| *	Merge remote-tracking branch 'OFFICIAL/trunk' into morefresh	Pierre Courtieu	2016-04-15
\| \| \|\ \| \|_\|/ \|/\| \|
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-04-09
\|\\| \|
\| * \|	Allow to unset the refinement mode of Instance in ML	Matthieu Sozeau	2016-04-07
\| * \|	Fixing an incorrect use of prod_appvect on a term which was not a	Hugo Herbelin	2016-04-07
\| * \|	Fixing the "No applicable tactic" non informative error message	Hugo Herbelin	2016-04-03
* \| \|	Moving Autorewrite back to tactics/.	Pierre-Marie Pédrot	2016-03-25
* \| \|	Moving Eqdecide to tactics/.	Pierre-Marie Pédrot	2016-03-25
* \| \|	Moving Eauto and Class_tactics to tactics/.	Pierre-Marie Pédrot	2016-03-25
* \| \|	Creating a dedicated ltac/ folder for Hightactics.	Pierre-Marie Pédrot	2016-03-21