coq - The formal proof system

Age	Commit message (Expand)	Author
2014-10-17	Experimental printing of the signature of open evars in Check.	Hugo Herbelin
2014-10-16	Goal: remove most of the API (make [Goal.goal] concrete).	Arnaud Spiwack
2014-10-13	Emit a warning for void Arguments statement (Close 3713)	Enrico Tassi
2014-10-13	library/opaqueTables: enable their use in interactive mode	Enrico Tassi
2014-10-11	Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name	Matthieu Sozeau
2014-10-09	Removing Convert_concl and Convert_hyp from Logic.	Hugo Herbelin
2014-10-01	Going back on granting wish #1039 in f5d7b2b1e so that apply with	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-29	Printing evar instance in a more intuitive order.	Hugo Herbelin
2014-09-29	Fix printing of primitive record info.	Matthieu Sozeau
2014-09-28	Print information about primitive records (Print and About).	Matthieu Sozeau
2014-09-25	Improve consistency of whitespace (beautifier).	Xavier Clerc
2014-09-24	Using an or_var rather than the hack with loc for coding a pure ident	Hugo Herbelin
2014-09-24	Fix a message.	Arnaud Spiwack
2014-09-24	coqtop -emacs: do not declare "still unfocused goals" as an "infomsg".	Arnaud Spiwack
2014-09-18	Fix debug printing with primitive projections.	Matthieu Sozeau
2014-09-17	Revert specific syntax for primitive projections, avoiding ugly	Matthieu Sozeau
2014-09-15	Add a "Hint Mode ref (+ \| -)*" hint for setting a global mode	Matthieu Sozeau
2014-09-15	Not printing goal name (reinstalled by mistake in a previous commit).	Hugo Herbelin
2014-09-15	Fixing bug #3619 in emacs mode.	Hugo Herbelin
2014-09-13	Prepare goal name printing but no not print them at the current time.	Hugo Herbelin
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	Use evar name to print goal.	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-12	Replace the list of argument in tacexpr with a single row argument.	Arnaud Spiwack
2014-09-10	VernacExtend does not dispatch on type anymore.	Pierre-Marie Pédrot
2014-09-08	Removing the XML plugin.	Pierre-Marie Pédrot
2014-09-08	Parsing of Type@{max(i,j)}.	Matthieu Sozeau
2014-09-05	Removing the old implementation of clear_body.	Pierre-Marie Pédrot
2014-09-04	Revert the two previous commits. I was testing in the wrong branch.	Pierre-Marie Pédrot
2014-09-04	Removing the old implementation of clear_body.	Pierre-Marie Pédrot
2014-09-04	Remove [Infer] option of records.	Arnaud Spiwack
2014-09-04	Inductive and CoInductive records are printed correctly.	Arnaud Spiwack
2014-09-04	Print [Variant] types with the keyword [Variant].	Arnaud Spiwack
2014-09-04	Add a [Variant] declaration which allows to write non-recursive variant types.	Arnaud Spiwack
2014-09-03	Fixing printing of unreachable local tactics.	Pierre-Marie Pédrot
2014-09-02	Cleaning code in Pptactic.	Pierre-Marie Pédrot
2014-09-02	Removing [revert] tactic from the AST.	Pierre-Marie Pédrot
2014-09-01	Moving the decompose tactic out of the AST.	Pierre-Marie Pédrot
2014-09-01	Coqide prints succesive hyps of the same type on 1 line	Pierre Boutillier
2014-08-30	Simplify even further the declaration of primitive projections,	Matthieu Sozeau
2014-08-29	Type-safe version of genarg list / pair / opt functions.	Pierre-Marie Pédrot
2014-08-29	Simplification of Genarg unpackers.	Pierre-Marie Pédrot
2014-08-25	"allows to", like "allowing to", is improper	Jason Gross
2014-08-21	Improve consistency of whitespace (beautifier).	Xavier Clerc
2014-08-21	Improve consistency of whitespace (beautifier).	Xavier Clerc