index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
Age
Commit message (
Expand
)
Author
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
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
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
2017-08-01
Binding more primitive tactics.
Pierre-Marie Pédrot
2017-08-01
Do not thunk notations preemptively.
Pierre-Marie Pédrot
2017-08-01
Adding new scopes for standard Ltac structures.
Pierre-Marie Pédrot
2017-07-30
Exporting more internals from Coq implementation.
Pierre-Marie Pédrot
2017-07-28
Parameterizing FFI functions for parameterized types.
Pierre-Marie Pédrot
2017-07-28
Moving the Ltac2 FFI to a separate file.
Pierre-Marie Pédrot
2017-07-28
Allowing generic patterns in let-bindings.
Pierre-Marie Pédrot
2017-07-27
Factorizing code for constructors and tuples.
Pierre-Marie Pédrot
2017-07-27
Cleaning up code in internalization.
Pierre-Marie Pédrot
2017-07-27
Fix expansion of toplevel let-rec after the constructor / constant split.
Pierre-Marie Pédrot
2017-07-27
Adding necessary primitives to do pattern-matching over constr.
Pierre-Marie Pédrot
2017-07-26
Tentative fix of parsing of product types.
Pierre-Marie Pédrot
2017-07-26
Dedicated module for ident type.
Pierre-Marie Pédrot
2017-07-26
Do not expand trivial patterns in functions.
Pierre-Marie Pédrot
2017-07-26
Ensuring that inductive constructors are always capitalized.
Pierre-Marie Pédrot
2017-07-26
Fix typo in error message
Pierre-Marie Pédrot
2017-07-26
Better typing errors for function types.
Pierre-Marie Pédrot
2017-07-26
Lightweight quotation syntax for terms and idents.
Pierre-Marie Pédrot
2017-07-26
Properly handling toplevel recursive definitions.
Pierre-Marie Pédrot
2017-07-26
Exporting some basic tactics from Ltac1.
Pierre-Marie Pédrot
2017-07-26
Bugfix: wrong access to non-constant constructor compilation.
Pierre-Marie Pédrot
2017-07-25
Generalizing patterns in fun bindings.
Pierre-Marie Pédrot
2017-07-24
Adding a few primitive functions.
Pierre-Marie Pédrot
2017-07-24
Correctly pushing variables for tuple patterns.
Pierre-Marie Pédrot
2017-07-24
Properly handle parsing of list patterns.
Pierre-Marie Pédrot
2017-07-24
Fix library hardwired prefix.
Pierre-Marie Pédrot
2017-07-24
Turning the ltac2 subfolder into a standalone plugin.
Pierre-Marie Pédrot
