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
*
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
*
|
|
Moving the "clearbody" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
|
|
Moving the "clear" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
|
|
Moving the "cofix" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
|
|
Moving the "fix" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
|
|
Removing the METAIDENT token, as it is not used anymore.
Pierre-Marie Pédrot
2016-02-24
[next]
Hugo Herbelin
Pierre-Marie Pédrot
Matthieu Sozeau