coq - The formal proof system

Age	Commit message (Expand)	Author
2015-02-23	Merge branch 'v8.5'	Pierre-Marie Pédrot
2015-02-19	Adding a possible DEPRECATED flag to VERNAC EXTEND statements.	Pierre-Marie Pédrot
2015-02-19	Record type for VERNAC EXTEND rules and a bit of documentation.	Pierre-Marie Pédrot
2015-01-27	Tentative fix for bug #3957.	Pierre-Marie Pédrot
2015-01-23	Splitting ML tactics in one function per grammar entry.	Pierre-Marie Pédrot
2015-01-21	Embedding the index of the ML tactic entry in the Tacexpr AST.	Pierre-Marie Pédrot
2015-01-12	Update headers.	Maxime Dénès
2014-12-23	A global [gfail] tactic which works like [fail] except that it fails even if ...	Arnaud Spiwack
2014-12-23	Fix compilation error in some configurations.	Arnaud Spiwack
2014-12-19	Add a backtracking version of Ltac's [match].	Arnaud Spiwack
2014-12-16	Fixing CAMLP4 compilation.	Pierre-Marie Pédrot
2014-12-12	Extend the syntax of simpl with a delta flag.	Arnaud Spiwack
2014-11-16	Enforcing a stronger difference between the two syntaxes "simpl	Hugo Herbelin
2014-11-09	Removing a unused boolean in the TacMove node of tacexpr AST.	Pierre-Marie Pédrot
2014-11-08	Continuing 3741c46fe134 on reporting ltac error.	Hugo Herbelin
2014-10-25	This commit introduces changes in induction and destruct.	Hugo Herbelin
2014-09-30	Seeing IntroWildcard as an action intro pattern rather than as a naming pattern	Hugo Herbelin
2014-09-30	Add syntax for naming new goals in refine: writing ?[id] instead of _	Hugo Herbelin
2014-09-12	Parsing evar instances.	Hugo Herbelin
2014-09-10	VernacExtend does not dispatch on type anymore.	Pierre-Marie Pédrot
2014-09-08	Parsing of Type@{max(i,j)}.	Matthieu Sozeau
2014-09-06	Renaming goal-entering functions.	Pierre-Marie Pédrot
2014-08-31	Moving code of tactic interpretation from Tacenv to Vernacentries.	Pierre-Marie Pédrot
2014-08-18	Reorganisation of intropattern code	Hugo Herbelin
2014-08-18	Moving the TacExtend node from atomic to plain tactics.	Pierre-Marie Pédrot
2014-08-07	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-06	Removing "intros untils" from the AST.	Pierre-Marie Pédrot
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-04	STM: encapsulate Pp.message in Feedback.feedback	Carst Tankink
2014-07-27	Qualified ML tactic names. The plugin name is used to discriminate	Pierre-Marie Pédrot
2014-07-25	Removing dead code relative to or_metaid.	Pierre-Marie Pédrot
2014-07-24	Distinguish tactics t1;t2 and t1;[t2..].	Arnaud Spiwack
2014-07-07	Fix g_coqast for explicit applications.	Matthieu Sozeau
2014-06-25	all coqide specific files moved into ide/	Enrico Tassi
2014-06-06	Moving the [split] tactic out of the AST.	Pierre-Marie Pédrot
2014-05-24	Fixing TACTIC EXTEND for arguments-free tactics that may modify the whole	Pierre-Marie Pédrot
2014-05-22	Removing useless use of metaids in tactic AST.	Pierre-Marie Pédrot
2014-05-21	Moving left & right tactics out of the AST.	Pierre-Marie Pédrot
2014-05-20	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-17	Fixing Camlp4 compilation	Pierre-Marie Pédrot
2014-05-16	Moving argument-free tactics out of the AST into a dedicated	Pierre-Marie Pédrot
2014-05-16	Tactics defined through TACTIC EXTEND that are only defined as a string do	Pierre-Marie Pédrot
2014-05-12	Now parsing rules of ML-declared tactics are only made available after the	Pierre-Marie Pédrot
2014-05-12	Moving the ML tactic extension mechanism to a Libobject-based one.	Pierre-Marie Pédrot
2014-05-12	Plugin names must be declared in the header of .ml4 file, be they static or	Pierre-Marie Pédrot