index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
tac2entries.ml
Age
Commit message (
Expand
)
Author
2017-08-18
Exporting scopes for occurrences.
Pierre-Marie Pédrot
2017-08-11
Introducing a syntax for goal dispatch.
Pierre-Marie Pédrot
2017-08-07
Introducing grammar-free tactic notations.
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
Introducing notations for destruct and induction arguments.
Pierre-Marie Pédrot
2017-08-02
Tentatively implementing apply.
Pierre-Marie Pédrot
2017-08-02
Extending the set of tactic scopes.
Pierre-Marie Pédrot
2017-08-01
Introducing the all-mighty intro-patterns.
Pierre-Marie Pédrot
2017-08-01
Adding new scopes for standard Ltac structures.
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-26
Ensuring that inductive constructors are always capitalized.
Pierre-Marie Pédrot
2017-07-26
Properly handling toplevel recursive definitions.
Pierre-Marie Pédrot
2017-07-24
Turning the ltac2 subfolder into a standalone plugin.
Pierre-Marie Pédrot
