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 PR #7016: Make parsing independent of the cumulativity flag.
Enrico Tassi
2018-04-05
|
\
*
\
Merge PR #7138: [stm] Move VernacBacktrack to the toplevel.
Enrico Tassi
2018-04-04
|
\
\
|
*
|
[stm] Move VernacBacktrack to the toplevel.
Emilio Jesus Gallego Arias
2018-04-01
*
|
|
Remove deprecated commands Arguments Scope and Implicit Arguments
Jasper Hugunin
2018-03-30
|
/
/
|
*
bool option -> (VernacCumulative | VernacNonCumulative) option
Gaëtan Gilbert
2018-03-22
|
*
Make parsing independent of the cumulativity flag.
Gaëtan Gilbert
2018-03-21
*
|
[vernac] Move `Quit` and `Drop` to the toplevel layer.
Emilio Jesus Gallego Arias
2018-03-11
|
/
*
[located] Push inner locations in `reference` to a CAst.t node.
Emilio Jesus Gallego Arias
2018-03-09
*
[located] More work towards using CAst.t
Emilio Jesus Gallego Arias
2018-03-09
*
Implement the Export Set/Unset feature.
Pierre-Marie Pédrot
2018-03-09
*
Merge PR #6909: Deprecate Focus and Unfocus
Maxime Dénès
2018-03-08
|
\
*
\
Merge PR #6790: Allow universe declarations for [with Definition].
Maxime Dénès
2018-03-07
|
\
\
|
*
|
Allow universe declarations for [with Definition].
Gaëtan Gilbert
2018-03-05
|
|
*
Deprecate Focus and Unfocus.
Théo Zimmermann
2018-03-05
*
|
|
Merge PR #6855: Update headers following #6543.
Maxime Dénès
2018-03-05
|
\
\
\
|
|
/
/
|
/
|
|
*
|
|
Merge PR #6791: Removing compatibility support for versions older than 8.5.
Maxime Dénès
2018-03-04
|
\
\
\
*
\
\
\
Merge PR #6736: [toplevel] Move beautify to its own pass.
Maxime Dénès
2018-03-04
|
\
\
\
\
|
|
_
|
_
|
/
|
/
|
|
|
|
|
*
|
Remove 8.5 compatibility support.
Théo Zimmermann
2018-03-02
|
|
*
|
Remove VOld compatibility flag.
Théo Zimmermann
2018-03-02
|
|
/
/
|
/
|
|
*
|
|
Merge PR #6864: Remove empty, wrongly located, doc file.
Maxime Dénès
2018-03-01
|
\
\
\
|
|
*
|
[toplevel] Move beautify to its own pass.
Emilio Jesus Gallego Arias
2018-02-28
|
|
/
/
|
/
|
|
*
|
|
Merge PR #6812: Rename release_lexer_state to the more descriptive get_lexer_...
Maxime Dénès
2018-02-28
|
\
\
\
|
|
*
|
Remove empty, wrongly located, doc file.
Théo Zimmermann
2018-02-28
|
|
/
/
|
/
|
|
|
|
*
Update headers following #6543.
Théo Zimmermann
2018-02-27
|
|
/
|
/
|
|
*
Rename release_lexer_state to the more descriptive get_lexer_state.
Jim Fehrle
2018-02-22
*
|
[ast] Improve precision of Ast location recognition in serialization.
Emilio Jesus Gallego Arias
2018-02-22
*
|
Trying a hack to support {'pat|P} without breaking compatibility.
Hugo Herbelin
2018-02-20
*
|
Change default for notations with variables bound to both terms and binders.
Hugo Herbelin
2018-02-20
*
|
Notations: Adding modifiers to tell which kind of binder a constr can parse.
Hugo Herbelin
2018-02-20
*
|
Notations: A step in cleaning constr_entry_key.
Hugo Herbelin
2018-02-20
*
|
Moving Metasyntax.register_grammar to Pcoq for usability in Egramcoq.
Hugo Herbelin
2018-02-20
*
|
Adding support for parsing subterms of a notation as "pattern".
Hugo Herbelin
2018-02-20
*
|
Adding patterns in the category of binders for notations.
Hugo Herbelin
2018-02-20
*
|
Renaming binders into binderlists in egramcoq.ml.
Hugo Herbelin
2018-02-20
*
|
Introducing an intermediary type "constr_prod_entry_key" for grammar producti...
Hugo Herbelin
2018-02-20
*
|
Rephrasing ETBinderList with a self-documenting and invariant-carrying argument.
Hugo Herbelin
2018-02-20
|
/
*
Change references to CAMLP4 to CAMLP5 to be more accurate since we no
Jim Fehrle
2018-02-17
*
[vernac] Mutual theorems (VernacStartTheoremProof) always have names
Vincent Laporte
2018-02-01
*
[vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinition
Vincent Laporte
2018-02-01
*
[vernac] vernac_expr no longer recursive
Vincent Laporte
2018-01-08
*
Merge PR #6433: [flags] Move global time flag into an attribute.
Maxime Dénès
2017-12-29
|
\
*
|
[api] Also deprecate constructors of Decl_kinds.
Emilio Jesus Gallego Arias
2017-12-23
|
*
[flags] Move global time flag into an attribute.
Emilio Jesus Gallego Arias
2017-12-23
|
/
*
Separate vernac controls and regular commands.
Maxime Dénès
2017-12-20
*
Merge PR #978: In printing, experimenting factorizing "match" clauses with sa...
Maxime Dénès
2017-12-14
|
\
|
*
Removing cumbersome location in multiple patterns.
Hugo Herbelin
2017-12-12
*
|
[summary] Allow typed projections from global state + rework of internals.
Emilio Jesus Gallego Arias
2017-12-09
|
/
*
Proper nametab handling of global universe names
Matthieu Sozeau
2017-12-01
*
Remove "obsolete_locality" and fix STM vernac classification.
Maxime Dénès
2017-11-29
*
Merge PR #6253: Fixing inconsistent associativity of level 10 in the table of...
Maxime Dénès
2017-11-29
|
\
[next]