index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
_CoqProject
Age
Commit message (
Expand
)
Author
2018-11-13
Port to coqpp.
Pierre-Marie Pédrot
2018-07-23
Adding environment-manipulating functions.
Pierre-Marie Pédrot
2017-12-26
adapt to API.mli removal
Enrico Tassi
2017-11-06
Generalize the use of repr in Tac2stdlib.
Pierre-Marie Pédrot
2017-10-27
Stubs for goal matching: quotation and matching function.
Pierre-Marie Pédrot
2017-10-01
Moving ML types used by Ltac2 to their proper interface.
Pierre-Marie Pédrot
2017-08-29
Rolling our own dynamic types for Ltac2.
Pierre-Marie Pédrot
2017-08-29
Binding primitives to generate fresh variables.
Pierre-Marie Pédrot
2017-08-18
Laxer dependencies between file and link reordering.
Pierre-Marie Pédrot
2017-08-02
Tentatively implementing apply.
Pierre-Marie Pédrot
2017-08-02
Adding a few standard notations for Ltac1 tactics.
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
Moving the Ltac2 FFI to a separate file.
Pierre-Marie Pédrot
2017-07-27
Adding necessary primitives to do pattern-matching over constr.
Pierre-Marie Pédrot
2017-07-26
Dedicated module for ident type.
Pierre-Marie Pédrot
2017-07-26
Exporting some basic tactics from Ltac1.
Pierre-Marie Pédrot
2017-07-24
Turning the ltac2 subfolder into a standalone plugin.
Pierre-Marie Pédrot
