coq - The formal proof system

Age	Commit message (Expand)	Author
2015-07-22	Removing the G_xml module again.	Pierre-Marie Pédrot
2015-07-01	Notation: use same level for "@" in constr: and pattern: (Close: #4272)	Enrico Tassi
2015-06-26	Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"	Lionel Rieg
2015-06-16	Granting, undocumentedly, parsing of "Conjectures" as a synonym of	Hugo Herbelin
2015-05-04	Add a [Redirect] vernacular command	Clément Pit--Claudel
2015-04-23	Remove almost all the uses of string concatenation when building error messages.	Guillaume Melquiond
2015-04-20	Inlining "fun" and "forall" tokens in parser, so that alternative notations for	Hugo Herbelin
2015-03-30	grammar: export constr_eval	Enrico Tassi
2015-03-30	grammar: export hypident	Enrico Tassi
2015-03-27	Putting the From parameter of the Require command into the AST.	Pierre-Marie Pédrot
2015-03-22	Qed export -> Qed exporting	Enrico Tassi
2015-02-23	Fixed 3233 (fresh does not work with a qualid).	Pierre Courtieu
2015-02-14	Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior	Enrico Tassi
2015-02-12	Fixing #3982 (conflict with max notation for universes).	Hugo Herbelin
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-19	Better doc and a few fixes for Proof using.	Enrico Tassi
2014-12-18	Proof using: New vernacular to name sets of section variables	Enrico Tassi
2014-12-16	Fixing CAMLP4 compilation.	Pierre-Marie Pédrot
2014-12-16	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot
2014-12-15	About now accepts hypothesis names and goal selector.	Pierre Courtieu
2014-12-12	Add Ltac syntax for the [tclIFCATCH] primitive.	Arnaud Spiwack
2014-12-12	Extend the syntax of simpl with a delta flag.	Arnaud Spiwack
2014-12-12	Searchxxx now search also the hypothesis and support goal selector.	Pierre Courtieu
2014-12-09	Switch the few remaining iso-latin-1 files to utf8	Pierre Letouzey
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-06	Fixing bugs #3723 and #3787 (reinitialization of camlp5 empty levels)	Hugo Herbelin
2014-11-02	Supporting "at occs" as a short-hand for "in \|- * at occs" in "destruct".	Hugo Herbelin
2014-11-01	Add [Info] command.	Arnaud Spiwack
2014-10-31	Reorganization of the test for generic selection of occurrences in	Hugo Herbelin
2014-10-27	Dead code	Hugo Herbelin
2014-10-25	This commit introduces changes in induction and destruct.	Hugo Herbelin
2014-10-13	Emit a warning for void Arguments statement (Close 3713)	Enrico Tassi
2014-10-13	Parsing of "?[" as two tokens (makes ssr compile).	Enrico Tassi
2014-10-07	Fixing #3687 (inconsistent lexer state after a bullet).	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-29	Notation: option to attach extra pretty printing rules to notations	Enrico Tassi
2014-09-24	Using an or_var rather than the hack with loc for coding a pure ident	Hugo Herbelin
2014-09-15	Add a "Hint Mode ref (+ \| -)*" hint for setting a global mode	Matthieu Sozeau
2014-09-13	Checking typability of evar instances. Using ";" to separate bindings	Hugo Herbelin
2014-09-12	Add syntax [id]: to apply tactic to goal named id.	Hugo Herbelin
2014-09-12	Parsing evar instances.	Hugo Herbelin
2014-09-12	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin
2014-09-10	VernacExtend does not dispatch on type anymore.	Pierre-Marie Pédrot
2014-09-08	Removing dead code relative to the XML plugin.	Pierre-Marie Pédrot
2014-09-08	Removing the XML plugin.	Pierre-Marie Pédrot