coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Reorganisation of intropattern code	Hugo Herbelin	2014-08-18
*	Refine patch for behavior of unify_to_subterm to allow backtracking on	Matthieu Sozeau	2014-08-18
*	Moving the TacAlias node out of atomic tactics.	Pierre-Marie Pédrot	2014-08-18
*	Moving the TacExtend node from atomic to plain tactics.	Pierre-Marie Pédrot	2014-08-18
*	A couple of fixes/improvements in -beautify, but backtracking on	Hugo Herbelin	2014-08-12
*	Removing simple induction / destruct from the AST.	Pierre-Marie Pédrot	2014-08-07
*	Instead of relying on a trick to make the constructor tactic parse, put	Pierre-Marie Pédrot	2014-08-07
*	Removing the "constructor" tactic from the AST.	Pierre-Marie Pédrot	2014-08-07
*	Removing "intros untils" from the AST.	Pierre-Marie Pédrot	2014-08-06
*	Fixing a few beautifying bugs.	Hugo Herbelin	2014-08-05
*	Experimentally adding an option for automatically erasing an	Hugo Herbelin	2014-08-05
*	Adding a syntax "enough" for the variant of "assert" with the order of	Hugo Herbelin	2014-08-05
*	New tactical [> t1…tn] to apply tactics t1…tn to the corresponding goal.	Arnaud Spiwack	2014-08-01
*	Add [numgoal] to Ltac.	Arnaud Spiwack	2014-08-01
*	Fix typo in cf04daec997.	Arnaud Spiwack	2014-08-01
*	Untyped terms in tactic: function [type_term c] to give a typed version of [c].	Arnaud Spiwack	2014-07-29
*	Add a type of untyped term to Ltac's value.	Arnaud Spiwack	2014-07-29
*	Qualified ML tactic names. The plugin name is used to discriminate	Pierre-Marie Pédrot	2014-07-27
*	Removing dead code relative to or_metaid.	Pierre-Marie Pédrot	2014-07-25
*	Distinguish tactics t1;t2 and t1;[t2..].	Arnaud Spiwack	2014-07-24
*	Adding a "time" tactical for benchmarking purposes. In case the tactic	Hugo Herbelin	2014-07-13
*	Revert "time tac" (committed by mistake).	Hugo Herbelin	2014-07-07
*	time tac	Hugo Herbelin	2014-07-07
*	Moving the [split] tactic out of the AST.	Pierre-Marie Pédrot	2014-06-06
*	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
*	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
*	Tentative to add constr-using primitive tactics without grammar rules.	Pierre-Marie Pédrot	2014-05-20
*	Moving argument-free tactics out of the AST into a dedicated	Pierre-Marie Pédrot	2014-05-16
*	Slightly better printer for native ML tactics, in order to disambiguate	Pierre-Marie Pédrot	2014-05-16
*	Closing bug #3260	Julien Forest	2014-04-14
*	Remove some dead-code (thanks to ocaml warnings)	Pierre Letouzey	2014-03-05
*	Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code	Pierre Letouzey	2014-03-02
*	Removing the useless pattern ident genarg.	Pierre-Marie Pédrot	2013-12-19
*	Printing function for Stdargs in debugger	Pierre Boutillier	2013-12-19
*	Removing RefArgType generic argument.	Pierre-Marie Pédrot	2013-12-01
*	Getting rid of casted_open_constr. It was only used by the	Pierre-Marie Pédrot	2013-11-30
*	Synchronizing the printer of tactic notations.	ppedrot	2013-11-13
*	Removing the dependency of every level of tactic ATSs on glob_tactic_expr.	ppedrot	2013-11-10
*	Revert the previous commit. It broke Coq compilation.	ppedrot	2013-11-09
*	Removing the dependency of every level of tactic ATSs on glob_tactic_expr.	ppedrot	2013-11-09
*	Update comments.	aspiwack	2013-11-02
*	Adds an experimental exactly_once tactical.	aspiwack	2013-11-02
*	Adds a tactical once.	aspiwack	2013-11-02
*	Added the tactical "tac1 + tac2".	aspiwack	2013-11-02
*	Fixing some tests from the test-suite.	ppedrot	2013-09-03
*	Removing SortArgType.	ppedrot	2013-07-05
*	Expurgating the useless difference between List0 and List1 at the	ppedrot	2013-07-05