index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
/
g_vernac.ml4
Commit message (
Expand
)
Author
Age
*
Revert "Better Arguments compatibility."
Maxime Dénès
2016-11-03
*
Merge branch 'v8.6' into trunk
Maxime Dénès
2016-11-03
|
\
|
*
Better Arguments compatibility.
Maxime Dénès
2016-11-02
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-29
|
\
|
|
*
Complete overhaul of the Arguments vernacular.
Maxime Dénès
2016-10-27
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-08
|
\
|
|
*
Do not add "Append" as a lexer keyword.
Pierre-Marie Pédrot
2016-10-06
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-05
|
\
|
|
*
Revert "Move bullet detection from lexer to parser (bug #5102)."
Guillaume Melquiond
2016-10-05
|
*
Merge remote-tracking branch 'github/pr/305' into v8.6
Maxime Dénès
2016-10-04
|
|
\
*
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-02
|
\
|
|
|
*
|
Move bullet detection from lexer to parser (bug #5102).
Guillaume Melquiond
2016-10-02
|
|
*
Add command 'Set foo Append "bar"' for appending to an option (bug #5109).
Guillaume Melquiond
2016-10-01
|
|
/
|
*
Merge remote-tracking branch 'github/pr/299' into v8.6
Maxime Dénès
2016-09-30
|
|
\
|
*
|
Fix bug #4798: compat notations should not modify the parser.
Pierre-Marie Pédrot
2016-09-29
|
*
|
Arguments: cleanup + detect discrepancy rename/implicit (#3753)
Enrico Tassi
2016-09-29
|
|
*
Fix bug #4869, allow Prop, Set, and level names in constraints.
Matthieu Sozeau
2016-09-29
|
|
/
*
|
Moving Ltac-specific parsing API to ltac/ folder.
Pierre-Marie Pédrot
2016-09-14
*
|
Make the user_err header an optional parameter.
Emilio Jesus Gallego Arias
2016-08-19
|
/
*
restore compatibility with gallium's camlp4 (broken by commit 8e07227c)
Pierre Letouzey
2016-07-26
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
A new infrastructure for warnings.
Maxime Dénès
2016-06-29
*
Adding ability to put any pattern in binders, prefixed by a quote.
Daniel de Rauglaudre
2016-06-27
*
Adding an only printing flag to notations.
Pierre-Marie Pédrot
2016-06-07
*
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
*
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
*
|
Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...
Matthieu Sozeau
2016-04-04
|
\
\
*
|
|
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 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
*
|
|
Moving Autorewrite to Hightatctic.
Pierre-Marie Pédrot
2016-03-06
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-29
|
\
\
\
|
|
|
/
|
|
/
|
|
*
|
Implement support for universe binder lists in Instance and Program Fixpoint/...
Matthieu Sozeau
2016-01-23
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
|
|
*
|
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
|
Simplification of grammar_prod_item type.
Pierre-Marie Pédrot
2016-01-02
*
|
|
ALPHA-CONVERSION: in "parsing/g_vernac.ml4" file
Matej Kosik
2015-12-18
*
|
|
CLEANUP: Vernacexpr.vernac_expr
Matej Kosik
2015-12-18
|
/
/
*
|
Allowing empty bound universe variables.
Pierre-Marie Pédrot
2015-10-08
*
|
Axioms now support the universe binding syntax.
Pierre-Marie Pédrot
2015-10-08
*
|
Proof using: let-in policy, optional auto-clear, forward closure*
Enrico Tassi
2015-10-08
*
|
Record fields accept an optional final semicolon separator.
Pierre-Marie Pédrot
2015-10-07
*
|
Univs: Add universe binding lists to definitions
Matthieu Sozeau
2015-09-14
*
|
Hacking parser so as to support both [> ... ] and [id].
Hugo Herbelin
2015-09-08
|
*
Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080
Jason Gross
2015-08-14
|
/
*
Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"
Lionel Rieg
2015-06-26
[next]