git.annexia.org / goals.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 318cea9) | patch
Define *file() syntax for tactic constructors.
authorRichard W.M. Jones <rjones@redhat.com>
Mon, 23 Dec 2019 19:08:14 +0000 (19:08 +0000)
committerRichard W.M. Jones <rjones@redhat.com>
Mon, 23 Dec 2019 19:11:08 +0000 (19:11 +0000)
commitb14ff66c953e6a73e9ac2fe8d42dd68e92e58f53
treed11ae0d6fbcbc6ac3ad3c6ce55d99395f055dd25tree | snapshot
parent318cea9f1c7669d23d27fc362bf06b9aca1b61a1commit | diff
Define *file() syntax for tactic constructors.

Alternative syntaxes considered where ~file and &file.
src/ast.ml diff | blob | history
src/ast.mli diff | blob | history
src/eval.ml diff | blob | history
src/lexer.mll diff | blob | history
src/parser.mly diff | blob | history
tests/test1.gl diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.