index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
vernac
Commit message (
Expand
)
Author
Age
*
Merge PR #6816: Adding mention of shelved/given-up status in Show Existentials
Maxime Dénès
2018-03-08
|
\
*
\
Merge PR #6893: Cleanup UState API usage
Maxime Dénès
2018-03-08
|
\
\
*
|
|
[vernac] Warn when using “Require” in a section
Vincent Laporte
2018-03-07
*
|
|
Merge PR #6790: Allow universe declarations for [with Definition].
Maxime Dénès
2018-03-07
|
\
\
\
*
\
\
\
Merge PR #6462: Sanitize universe declaration in Context (stop using a ref...)
Maxime Dénès
2018-03-07
|
\
\
\
\
|
|
|
*
|
Rename some universe minimizing "normalize" functions to "minimize"
Gaëtan Gilbert
2018-03-06
|
|
|
*
|
Deprecate UState aliases in Evd.
Gaëtan Gilbert
2018-03-06
|
|
_
|
/
/
|
/
|
|
|
*
|
|
|
Merge PR #6749: Fixing an anomaly in the presence of "let-in" in the type of ...
Maxime Dénès
2018-03-06
|
\
\
\
\
*
\
\
\
\
Merge PR #6896: [compat] Remove NOOP deprecated options.
Maxime Dénès
2018-03-06
|
\
\
\
\
\
|
|
|
|
*
|
Allow universe declarations for [with Definition].
Gaëtan Gilbert
2018-03-05
|
|
|
*
|
|
Sanitize universe declaration in Context (stop using a ref...)
Gaëtan Gilbert
2018-03-05
|
|
|
|
/
/
*
|
|
|
|
Merge PR #6855: Update headers following #6543.
Maxime Dénès
2018-03-05
|
\
\
\
\
\
|
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
*
|
|
[compat] Remove NOOP and alias deprecated options.
Emilio Jesus Gallego Arias
2018-03-04
|
|
/
/
/
|
/
|
|
|
*
|
|
|
Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.
Maxime Dénès
2018-03-04
|
\
\
\
\
*
\
\
\
\
Merge PR #6676: [proofview] goals come with a state
Maxime Dénès
2018-03-04
|
\
\
\
\
\
*
|
|
|
|
|
[toplevel] [vernac] Remove Load hack and check supported scenarios.
Emilio Jesus Gallego Arias
2018-02-28
|
|
*
|
|
|
[econstr] Continue consolidation of EConstr API under `interp`.
Emilio Jesus Gallego Arias
2018-02-28
|
|
/
/
/
/
|
/
|
|
|
|
|
|
*
|
|
Update headers following #6543.
Théo Zimmermann
2018-02-27
|
|
/
/
/
|
/
|
|
|
*
|
|
|
Merge PR #6784: New IR in VM: Clambda
Maxime Dénès
2018-02-24
|
\
\
\
\
|
*
|
|
|
New IR in VM: Clambda.
Maxime Dénès
2018-02-23
|
|
|
|
*
Adding mention of shelved/given-up status in "Show Existentials".
Hugo Herbelin
2018-02-22
*
|
|
|
|
[ast] Improve precision of Ast location recognition in serialization.
Emilio Jesus Gallego Arias
2018-02-22
|
|
_
|
_
|
/
|
/
|
|
|
*
|
|
|
Merge PR #6767: [ci] add elpi
Maxime Dénès
2018-02-21
|
\
\
\
\
*
\
\
\
\
Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585)
Maxime Dénès
2018-02-21
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #6748: Fix bug #6529: nf_evar_info to nf the evars' env not just the...
Maxime Dénès
2018-02-21
|
\
\
\
\
\
\
|
|
_
|
_
|
/
/
/
|
/
|
|
|
|
|
|
|
|
|
*
|
proofview: goals come with a state
Enrico Tassi
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
|
|
*
|
|
More flexibility in locating or referring to a notation.
Hugo Herbelin
2018-02-20
|
|
*
|
|
Being more flexible on format Adding a warning to be more informative
Hugo Herbelin
2018-02-20
|
|
*
|
|
Respecting the ident/pattern distinction in notation modifiers.
Hugo Herbelin
2018-02-20
|
|
*
|
|
Adding support for parsing subterms of a notation as "pattern".
Hugo Herbelin
2018-02-20
|
|
*
|
|
A bit of miscellaneous code documentation around notations.
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
|
|
*
|
|
More precise explanation when a notation is not reversible for printing.
Hugo Herbelin
2018-02-20
|
|
/
/
/
|
/
|
|
|
|
|
*
|
record: restore API declare_projections (removed in e414c07e1)
Enrico Tassi
2018-02-19
|
|
/
/
|
/
|
|
*
|
|
Merge PR #6761: Remove unused argument in Record.declare_structure
Maxime Dénès
2018-02-19
|
\
\
\
|
|
*
|
Fix #6529: nf_evar_info and check the env evars' not just the concl
Matthieu Sozeau
2018-02-19
*
|
|
|
Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ...
Maxime Dénès
2018-02-19
|
\
\
\
\
|
|
_
|
/
/
|
/
|
|
|
|
*
|
|
Change references to CAMLP4 to CAMLP5 to be more accurate since we no
Jim Fehrle
2018-02-17
|
|
*
|
Remove unused argument in Record.declare_structure
Gaëtan Gilbert
2018-02-14
|
|
/
/
|
/
|
|
|
|
*
Fixing an anomaly in the presence of "let-in" in the type of a record.
Hugo Herbelin
2018-02-13
*
|
|
Merge PR #6702: [vernac] [minor] Move print effects to top-level caller.
Maxime Dénès
2018-02-13
|
\
\
\
|
|
_
|
/
|
/
|
|
*
|
|
Merge PR #6262: [error] Replace msg_error by a proper exception.
Maxime Dénès
2018-02-12
|
\
\
\
*
\
\
\
Merge PR #6128: Simplification: cumulativity information is variance informa...
Maxime Dénès
2018-02-12
|
\
\
\
\
|
*
|
|
|
Use specialized function for inductive subtyping inference.
Gaëtan Gilbert
2018-02-11
|
*
|
|
|
Inference of inductive subtyping does not need an evar map.
Gaëtan Gilbert
2018-02-10
[next]