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-29
Removing dead code for handling of array litterals.
Pierre-Marie Pédrot
2017-08-29
Factorizing code for declaration of primitive tactics.
Pierre-Marie Pédrot
2017-08-29
Implementing Ltac2 antiquotations in constr syntax.
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-28
Fix coq/ltac2#6: Expected and actual types are flipped.
Pierre-Marie Pédrot
2017-08-27
Do not reuse the Val.t type in toplevel values.
Pierre-Marie Pédrot
2017-08-27
Ensure no confusion with unit in rigid variables.
Pierre-Marie Pédrot
2017-08-27
Proper handling of rigid variables in subtyping.
Pierre-Marie Pédrot
2017-08-27
Introducing rebindable toplevel definitions.
Pierre-Marie Pédrot
2017-08-26
Allowing calls to Ltac2 inside Ltac1.
Pierre-Marie Pédrot
2017-08-26
Allowing to insert calls to Ltac1 references in Ltac2.
Pierre-Marie Pédrot
2017-08-25
Introducing a distinct bindings scope.
Pierre-Marie Pédrot
2017-08-25
Renaming the bindings scope into with_bindings.
Pierre-Marie Pédrot
2017-08-25
Do not return STRING scopes in the tuple produced by "seq" scopes.
Pierre-Marie Pédrot
2017-08-25
More bindings to primitive tactics.
Pierre-Marie Pédrot
2017-08-25
Respect the default goal selector in toplevel invocations.
Pierre-Marie Pédrot
2017-08-25
Parse specifically idents as destruction arguments.
Pierre-Marie Pédrot
2017-08-25
Lookahead to cheat the constr parser in order to parse "& IDENT".
Pierre-Marie Pédrot
2017-08-24
Removing dead code about arrays in the AST.
Pierre-Marie Pédrot
2017-08-24
Rely on quoting for lists instead of hardwiring it in the AST.
Pierre-Marie Pédrot
2017-08-24
Adding a notation scope for global references.
Pierre-Marie Pédrot
2017-08-24
Fix typing of reference quotations.
Pierre-Marie Pédrot
2017-08-24
Adding a scope for reduction flags.
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
More precise type for quotation entries.
Pierre-Marie Pédrot
2017-08-18
Removing dead code.
Pierre-Marie Pédrot
2017-08-18
Laxer dependencies between file and link reordering.
Pierre-Marie Pédrot
2017-08-18
Exporting scopes for occurrences.
Pierre-Marie Pédrot
2017-08-18
Trying to enhance the printing of tactic expressions.
Pierre-Marie Pédrot
2017-08-11
Introducing a syntax for goal dispatch.
Pierre-Marie Pédrot
2017-08-08
Another batch of primitive operations.
Pierre-Marie Pédrot
2017-08-08
Code simplification in quotations.
Pierre-Marie Pédrot
2017-08-07
Fix location of not-unit warning.
Pierre-Marie Pédrot
2017-08-07
Fix parsing of parenthesized expressions.
Pierre-Marie Pédrot
2017-08-07
Defining a few base tacticals.
Pierre-Marie Pédrot
2017-08-07
Introducing grammar-free tactic notations.
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
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
[next]
