coq - The formal proof system

Age	Commit message (Collapse)	Author
2017-08-25	Introducing a distinct bindings scope.	Pierre-Marie Pédrot

2017-08-25	Renaming the bindings scope into with_bindings.	Pierre-Marie Pédrot

2017-08-25	Do not return STRING scopes in the tuple produced by "seq" scopes.	Pierre-Marie Pédrot

2017-08-25	More bindings to primitive tactics.	Pierre-Marie Pédrot

2017-08-25	Respect the default goal selector in toplevel invocations.	Pierre-Marie Pédrot

2017-08-25	Parse specifically idents as destruction arguments.	Pierre-Marie Pédrot
	This is for backward compatibility.
2017-08-25	Lookahead to cheat the constr parser in order to parse "& IDENT".	Pierre-Marie Pédrot

2017-08-24	Removing dead code about arrays in the AST.	Pierre-Marie Pédrot

2017-08-24	Rely on quoting for lists instead of hardwiring it in the AST.	Pierre-Marie Pédrot

2017-08-24	Adding a notation scope for global references.	Pierre-Marie Pédrot

2017-08-24	Fix typing of reference quotations.	Pierre-Marie Pédrot

2017-08-24	Adding a scope for reduction flags.	Pierre-Marie Pédrot

2017-08-24	Introducing a quotation for global references.	Pierre-Marie Pédrot

2017-08-24	Use references in reduction tactics.	Pierre-Marie Pédrot
	We dynamically check that the provided references are indeed evaluable ones, instead of ensuring this at internalization time.
2017-08-18	More precise type for quotation entries.	Pierre-Marie Pédrot

2017-08-18	Removing dead code.	Pierre-Marie Pédrot

2017-08-18	Laxer dependencies between file and link reordering.	Pierre-Marie Pédrot

2017-08-18	Exporting scopes for occurrences.	Pierre-Marie Pédrot

2017-08-18	Trying to enhance the printing of tactic expressions.	Pierre-Marie Pédrot

2017-08-11	Introducing a syntax for goal dispatch.	Pierre-Marie Pédrot

2017-08-08	Another batch of primitive operations.	Pierre-Marie Pédrot

2017-08-08	Code simplification in quotations.	Pierre-Marie Pédrot

2017-08-07	Fix location of not-unit warning.	Pierre-Marie Pédrot

2017-08-07	Fix parsing of parenthesized expressions.	Pierre-Marie Pédrot

2017-08-07	Defining a few base tacticals.	Pierre-Marie Pédrot

2017-08-07	Introducing grammar-free tactic notations.	Pierre-Marie Pédrot

2017-08-05	Exporting more reduction functions.	Pierre-Marie Pédrot

2017-08-05	Exporting the rewrite tactic.	Pierre-Marie Pédrot

2017-08-04	Introducing quotations for the rewrite tactic.	Pierre-Marie Pédrot

2017-08-04	Adding locations to quotation types.	Pierre-Marie Pédrot

2017-08-04	More precise type for quoted structures.	Pierre-Marie Pédrot

2017-08-04	Adding the induction and destruct tactics.	Pierre-Marie Pédrot

2017-08-04	Introducing notations for destruct and induction arguments.	Pierre-Marie Pédrot

2017-08-02	Tentatively implementing apply.	Pierre-Marie Pédrot

2017-08-02	Properly implementing the notation to easily access hypotheses.	Pierre-Marie Pédrot

2017-08-02	Merging the e/- variants of primitive tactics.	Pierre-Marie Pédrot

2017-08-02	Adding new notations.	Pierre-Marie Pédrot

2017-08-02	Extending the set of tactic scopes.	Pierre-Marie Pédrot
	We now allow mere tokens, keywords and sequencing amongst others.
2017-08-02	Properly classifying Ltac2 notations.	Pierre-Marie Pédrot

2017-08-02	Fixing parsing of match branches.	Pierre-Marie Pédrot

2017-08-02	Removing deprecated stuff.	Pierre-Marie Pédrot

2017-08-02	Bindings use open constr quotations.	Pierre-Marie Pédrot

2017-08-02	Adding the open_constr scope	Pierre-Marie Pédrot

2017-08-02	Tentatively fixing a few parsing issues.	Pierre-Marie Pédrot

2017-08-02	Fixup reification of egeneralize.	Pierre-Marie Pédrot

2017-08-01	More primitive tactics.	Pierre-Marie Pédrot

2017-08-01	Expanding unification variables in typechecking error messages.	Pierre-Marie Pédrot

2017-08-01	Don't reuse Coq AST for binding quotations.	Pierre-Marie Pédrot
	This allows antiquotations in binding lists.
2017-08-01	Fix parsing of fresh ident antiquotations.	Pierre-Marie Pédrot

2017-08-01	Introducing the all-mighty intro-patterns.	Pierre-Marie Pédrot