index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
Commit message (
Expand
)
Author
Age
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-09
|
\
|
*
Rename Lexer -> CLexer.
Pierre-Marie Pédrot
2016-05-09
*
|
Removing dead code and unused opens.
Pierre-Marie Pédrot
2016-05-08
*
|
Removing useless generic arguments.
Pierre-Marie Pédrot
2016-05-04
*
|
Revert "In the short term, stronger invariant on the syntax of TacAssert, what"
Hugo Herbelin
2016-04-27
*
|
Revert "Fixing a mispelling coma -> comma."
Hugo Herbelin
2016-04-27
*
|
Fixing a mispelling coma -> comma.
Hugo Herbelin
2016-04-27
*
|
In the short term, stronger invariant on the syntax of TacAssert, what
Hugo Herbelin
2016-04-27
*
|
Removing dead code in Compat.
Pierre-Marie Pédrot
2016-04-25
*
|
Remove dead registering code in Pcoq.
Pierre-Marie Pédrot
2016-04-24
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-04-24
|
\
|
|
*
A fix to #4666 (Exc_located capsule added by camlp5 overwriting
Hugo Herbelin
2016-04-12
*
|
Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...
Matthieu Sozeau
2016-04-04
|
\
\
*
|
|
Getting rid of the "_mods" parsing entry.
Pierre-Marie Pédrot
2016-04-01
*
|
|
Moving the code handling tactic notations to Tacentries.
Pierre-Marie Pédrot
2016-03-31
*
|
|
Abstracting away the Summary-synchronized grammar-modifying commands.
Pierre-Marie Pédrot
2016-03-31
*
|
|
Moving the Tactic Notation entry parser from Pcoq to Tacentries.
Pierre-Marie Pédrot
2016-03-31
*
|
|
Adding a new Ltac generic argument for forced tactics returing unit.
Pierre-Marie Pédrot
2016-03-20
*
|
|
Moving the Ltac definition command to an EXTEND based command.
Pierre-Marie Pédrot
2016-03-20
*
|
|
Moving Print Ltac to an EXTEND based command.
Pierre-Marie Pédrot
2016-03-20
*
|
|
Moving Tactic Notation to an EXTEND based command.
Pierre-Marie Pédrot
2016-03-20
*
|
|
Moving Tacinterp to Hightactics.
Pierre-Marie Pédrot
2016-03-20
*
|
|
Fixing compilation with old versions of CAMLP5.
Pierre-Marie Pédrot
2016-03-19
*
|
|
Further reducing the dependencies of the EXTEND macros.
Pierre-Marie Pédrot
2016-03-19
*
|
|
Moving VernacSolve to an EXTEND-based definition.
Pierre-Marie Pédrot
2016-03-19
*
|
|
Moving the parsing of the Ltac proof mode to G_ltac.
Pierre-Marie Pédrot
2016-03-19
*
|
|
Moving the proof mode parsing management to Pcoq.
Pierre-Marie Pédrot
2016-03-19
*
|
|
Allowing generalized rules in typed symbols.
Pierre-Marie Pédrot
2016-03-19
*
|
|
Do not export entry_key from Pcoq anymore.
Pierre-Marie Pédrot
2016-03-19
*
|
|
Simplifying the code of Entry.
Pierre-Marie Pédrot
2016-03-19
*
|
|
Removing dead code in Pcoq.
Pierre-Marie Pédrot
2016-03-18
*
|
|
Making the EXTEND macros almost self-contained.
Pierre-Marie Pédrot
2016-03-18
*
|
|
ARGUMENT EXTEND made of only one entry share the same grammar.
Pierre-Marie Pédrot
2016-03-18
*
|
|
Removing the special status of generic arguments defined by Coq itself.
Pierre-Marie Pédrot
2016-03-17
*
|
|
Code factorization in Pcoq.
Pierre-Marie Pédrot
2016-03-17
*
|
|
Adding a universe argument to Pcoq.create_generic_entry.
Pierre-Marie Pédrot
2016-03-17
*
|
|
Relying on parsing rules rather than genarg to check if an argument is empty.
Pierre-Marie Pédrot
2016-03-17
*
|
|
Adopting the same rules for interpreting @, abbreviations and
Hugo Herbelin
2016-03-13
*
|
|
Supporting "(@foo) args" in patterns, where "@foo" has no arguments.
Hugo Herbelin
2016-03-13
*
|
|
Moving Autorewrite to Hightatctic.
Pierre-Marie Pédrot
2016-03-06
*
|
|
Fixing bug #4610: Fails to build with camlp4 since the TACTIC EXTEND move.
Pierre-Marie Pédrot
2016-03-06
*
|
|
Replacing ad-hoc tactic scopes by generic ones using [create_ltac_quotations].
Pierre-Marie Pédrot
2016-03-04
*
|
|
Exchanging roles of tactic_arg and tactic_top_or_arg entries.
Pierre-Marie Pédrot
2016-03-04
*
|
|
Removing the UConstr entry of the tactic_arg AST.
Pierre-Marie Pédrot
2016-03-04
*
|
|
Making parentheses mandatory in tactic scopes.
Pierre-Marie Pédrot
2016-03-04
*
|
|
Uniformizing the parsing of argument scopes in Ltac.
Pierre-Marie Pédrot
2016-03-04
*
|
|
Moving the "move" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
|
|
Moving the "exists" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
|
|
Moving the "symmetry" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
|
|
Moving the "generalize dependent" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
[next]
Pierre-Marie Pédrot
Hugo Herbelin
Matthieu Sozeau