index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
tac2stdlib.ml
Age
Commit message (
Expand
)
Author
2018-06-18
Fixing a batch of deprecation warnings.
Pierre-Marie Pédrot
2018-05-24
Adapt to fix/cofix changes in Coq (coq/coq#7196)
Emilio Jesus Gallego Arias
2018-04-02
[coq] Adapt to coq/coq#6960.
Emilio Jesus Gallego Arias
2017-11-06
Generalize the use of repr in Tac2stdlib.
Pierre-Marie Pédrot
2017-11-02
Binding the specialize tactic.
Pierre-Marie Pédrot
2017-10-30
Introducing the change tactic.
Pierre-Marie Pédrot
2017-10-07
Remove unused warnings.
Pierre-Marie Pédrot
2017-10-01
Using Ltac2 native closures in some tactic APIs.
Pierre-Marie Pédrot
2017-10-01
Rolling up our own representation of clauses.
Pierre-Marie Pédrot
2017-10-01
Moving ML types used by Ltac2 to their proper interface.
Pierre-Marie Pédrot
2017-09-30
Abstracting away the primitive functions on valexpr datatype.
Pierre-Marie Pédrot
2017-09-26
Adding quotations for the assert family of tactics.
Pierre-Marie Pédrot
2017-09-15
Making Ltac2 representation of data coincide with the ML-side one.
Pierre-Marie Pédrot
2017-09-14
Abstracting away the type of arities and ML tactics.
Pierre-Marie Pédrot
2017-09-14
Moving valexpr definition to Tac2ffi.
Pierre-Marie Pédrot
2017-09-14
Explicit arity for closures.
Pierre-Marie Pédrot
2017-09-14
Introducing the remember tactic.
Pierre-Marie Pédrot
2017-09-14
Binding the pose/set family of tactics.
Pierre-Marie Pédrot
2017-09-07
Communicate the backtrace through the monad.
Pierre-Marie Pédrot
2017-09-06
Using higher-order representation for closures.
Pierre-Marie Pédrot
2017-09-06
The interp_app function now takes a closure as an argument.
Pierre-Marie Pédrot
2017-09-05
Binding the firstorder tactic.
Pierre-Marie Pédrot
2017-09-05
Binding move and intro.
Pierre-Marie Pédrot
2017-09-05
Binding the inversion family of tactics.
Pierre-Marie Pédrot
2017-09-05
Typeclasses_eauto strategy is now optional.
Pierre-Marie Pédrot
2017-09-05
More static invariants for typeclass_eauto.
Pierre-Marie Pédrot
2017-09-05
ML bindings of auto-related tactics.
Pierre-Marie Pédrot
2017-09-04
Quick-and-dirty backtrace mechanism for the interpreter.
Pierre-Marie Pédrot
2017-08-30
Binding reduction functions acting on terms.
Pierre-Marie Pédrot
2017-08-25
More bindings to primitive tactics.
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
2017-08-18
Removing dead code.
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
Adding the induction and destruct tactics.
Pierre-Marie Pédrot
2017-08-02
Tentatively implementing apply.
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
Fixup reification of egeneralize.
Pierre-Marie Pédrot
2017-08-01
More primitive tactics.
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-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-26
Exporting some basic tactics from Ltac1.
Pierre-Marie Pédrot
