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 remote-tracking branch 'github/pr/212' into trunk
Maxime Dénès
2016-06-20
|
\
|
*
Add file name, line number and beginning of line position to locations.
Maxime Dénès
2016-06-20
*
|
Exporting a generic argument induction_arg. As a consequence,
Hugo Herbelin
2016-06-18
*
|
Adding eintros to respect the e- prefix policy.
Hugo Herbelin
2016-06-18
|
*
Set required version of camlp5 to 6.06.
Maxime Dénès
2016-06-17
|
/
*
Extend Hint Mode to handle the no-head-evar case
Matthieu Sozeau
2016-06-16
*
Fixing a mispelling coma -> comma.
Hugo Herbelin
2016-06-16
*
A stronger invariant on the syntax of TacAssert, what allows for a
Hugo Herbelin
2016-06-16
*
Adding an only printing flag to notations.
Pierre-Marie Pédrot
2016-06-07
*
Removing the use to Egramcoq.recover_constr_grammar.
Pierre-Marie Pédrot
2016-06-07
*
Removing "rename" from the tactic AST.
Pierre-Marie Pédrot
2016-06-03
*
Removing "exact" from the tactic AST.
Pierre-Marie Pédrot
2016-06-03
*
Removing "intro" from the tactic AST.
Pierre-Marie Pédrot
2016-06-03
*
Removing "double induction" from the tactic AST.
Pierre-Marie Pédrot
2016-06-03
*
g_tactics : remove opt_bindings (2-line dead code)
Pierre Letouzey
2016-06-01
*
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
*
The grammar_extend function now registers unsynchronized extensions.
Pierre-Marie Pédrot
2016-05-11
*
Making the grammar command extend API purely functional.
Pierre-Marie Pédrot
2016-05-11
*
Moving the constr empty entry registering to the state-based API.
Pierre-Marie Pédrot
2016-05-11
*
Turning the grammar extend command API into a state-passing one.
Pierre-Marie Pédrot
2016-05-11
*
Moving the grammar summary to Pcoq.
Pierre-Marie Pédrot
2016-05-11
*
Delimiting the use of unsafe code in Pcoq.
Pierre-Marie Pédrot
2016-05-10
*
Overlooked use of Gram instead of G module in Pcoq.
Pierre-Marie Pédrot
2016-05-10
*
Further tidying of the constr extension code.
Pierre-Marie Pédrot
2016-05-10
*
Type-safe constr notations.
Pierre-Marie Pédrot
2016-05-10
*
AlistNsep token now accepts an arbitrary separator.
Pierre-Marie Pédrot
2016-05-10
*
Simpler data structure for Arules token.
Pierre-Marie Pédrot
2016-05-10
*
Purer implementation of empty level registering in Pcoq.
Pierre-Marie Pédrot
2016-05-10
*
Removing the Entry module now that rules need not be marshalled.
Pierre-Marie Pédrot
2016-05-10
*
Hardening the obsolete unsafe_grammar_statement API.
Pierre-Marie Pédrot
2016-05-10
*
Removing dead code in Compat.
Pierre-Marie Pédrot
2016-05-10
*
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
[prev]
[next]