coq - The formal proof system

Age	Commit message (Expand)	Author
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
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-03-05	Adding a canary library. This canary is imperfect. It allows serialization	Pierre-Marie Pédrot
2014-03-05	Added a new module HMap. It works (almost) like Map, except that it expects	Pierre-Marie Pédrot
2014-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
2014-03-05	Adding a CSet module in Coq lib.	Pierre-Marie Pédrot
2014-03-02	Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code	Pierre Letouzey
2014-02-16	Removing non-marshallable data from the Agram constructor. Instead of	Pierre-Marie Pédrot