index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
theories
Age
Commit message (
Expand
)
Author
2019-01-28
Make lazy_match! goal actually lazy
Jason Gross
2018-11-19
Adding a module to manipulate Ltac1 values.
Pierre-Marie Pédrot
2018-11-19
Add a function to generate fresh reference instances.
Pierre-Marie Pédrot
2018-11-19
Add a Char module.
Pierre-Marie Pédrot
2018-07-23
Adding environment-manipulating functions.
Pierre-Marie Pédrot
2017-11-02
Fix the horrible syntax that used to be valid for tuple matching.
Pierre-Marie Pédrot
2017-11-02
Binding the specialize tactic.
Pierre-Marie Pédrot
2017-10-30
Add a macro for the now tactic
Pierre-Marie Pédrot
2017-10-30
Introducing the change tactic.
Pierre-Marie Pédrot
2017-10-27
Adding a notation for match goal.
Pierre-Marie Pédrot
2017-10-27
Stubs for goal matching: quotation and matching function.
Pierre-Marie Pédrot
2017-10-07
Implementing the Constr.in_context function.
Pierre-Marie Pédrot
2017-09-26
Adding quotations for the assert family of tactics.
Pierre-Marie Pédrot
2017-09-26
Slightly more straightforward notation for (e)apply.
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
Introducing the remember tactic.
Pierre-Marie Pédrot
2017-09-14
Binding the pose/set family of tactics.
Pierre-Marie Pédrot
2017-09-14
Use a simpler syntax for generalize grammar.
Pierre-Marie Pédrot
2017-09-13
Adding quotations for the generalize tactic.
Pierre-Marie Pédrot
2017-09-08
Fix coq/ltac2#24: There should be a way to turn an exn into a message.
Pierre-Marie Pédrot
2017-09-05
Binding the firstorder tactic.
Pierre-Marie Pédrot
2017-09-05
Export Ltac2.Notations in the Ltac2 entry module.
Pierre-Marie Pédrot
2017-09-05
The absurd tactic now parses a constr.
Pierre-Marie Pédrot
2017-09-05
Binding move and intro.
Pierre-Marie Pédrot
2017-09-05
Introducing quotations for move locations.
Pierre-Marie Pédrot
2017-09-05
Binding the inversion family of tactics.
Pierre-Marie Pédrot
2017-09-05
A few more notations.
Pierre-Marie Pédrot
2017-09-05
Typeclasses_eauto strategy is now optional.
Pierre-Marie Pédrot
2017-09-05
Fixup grammar of typeclasses_eauto.
Pierre-Marie Pédrot
2017-09-05
Quotations for auto-related tactics.
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
Notation for "clear - ids".
Pierre-Marie Pédrot
2017-09-04
More notations for primitive tactics.
Pierre-Marie Pédrot
2017-09-04
Implementing multi-match and simple match over constrs.
Pierre-Marie Pédrot
2017-09-04
Implementing lazy matching over terms.
Pierre-Marie Pédrot
2017-09-03
Introducing a macro for constr matching.
Pierre-Marie Pédrot
2017-09-02
Fix coq/ltac2#15: Ltac2 scope cannot be disabled after it is required.
Pierre-Marie Pédrot
2017-09-01
Passing an optional message to Tactic_failure.
Pierre-Marie Pédrot
2017-08-31
Properly handling internal errors from Coq.
Pierre-Marie Pédrot
2017-08-31
Expand the primitive functions on terms.
Pierre-Marie Pédrot
2017-08-31
Require Ltac2.Fresh in Ltac2.Ltac2
Jason Gross
2017-08-31
Fix the type of the Constructor constructor.
Pierre-Marie Pédrot
2017-08-30
Binding reduction functions acting on terms.
Pierre-Marie Pédrot
2017-08-29
Binding an unsafe substitution function.
Pierre-Marie Pédrot
2017-08-29
Binding primitives to generate fresh variables.
Pierre-Marie Pédrot
2017-08-27
Notation for clear.
Pierre-Marie Pédrot
2017-08-27
Fix semantics of the solve tactical.
Pierre-Marie Pédrot
2017-08-25
Adding more notations for the lulz.
Pierre-Marie Pédrot
2017-08-25
Renaming the bindings scope into with_bindings.
Pierre-Marie Pédrot
[next]
