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 #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
|
/
/
*
|
Merge PR #7062: Slightly refining some error messages about unresolvable evars.
Pierre-Marie Pédrot
2018-03-27
|
\
\
|
*
|
Slightly refining some error messages about unresolvable evars.
Hugo Herbelin
2018-03-24
|
|
*
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
*
Merge PR #6775: Allow using cumulativity without forcing strict constraints.
Maxime Dénès
2018-03-09
|
\
*
\
Merge PR #6923: Export options
Maxime Dénès
2018-03-09
|
\
\
|
|
*
Allow using cumulativity without forcing strict constraints.
Gaëtan Gilbert
2018-03-09
|
*
|
Implement the Export Set/Unset feature.
Pierre-Marie Pédrot
2018-03-09
|
*
|
Export the various option localities in the API.
Pierre-Marie Pédrot
2018-03-09
|
|
/
*
/
allow Prop as source for coercions
charguer
2018-03-09
|
/
*
Merge PR #6941: [toplevel] Respect COQ_COLORS environment variable
Maxime Dénès
2018-03-09
|
\
*
\
Merge PR #6945: Fix error with univ binders on monomorphic records.
Maxime Dénès
2018-03-09
|
\
\
*
\
\
Merge PR #407: Fix SR breakage due to allowing fixpoints on non-rec values
Maxime Dénès
2018-03-09
|
\
\
\
*
\
\
\
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
|
\
\
\
\
\
|
|
|
|
*
|
Fix error with univ binders on monomorphic records.
Gaëtan Gilbert
2018-03-08
|
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
|
*
|
Fix SR breakage due to allowing fixpoints on non-rec values
Matthieu Sozeau
2018-03-08
|
|
|
|
*
[toplevel] Respect COQ_COLORS environment variable
Thomas Hebb
2018-03-07
*
|
|
|
|
[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
[next]
Enrico Tassi
Emilio Jesus Gallego Arias
Jasper Hugunin
Pierre-Marie Pédrot
Hugo Herbelin
Gaëtan Gilbert
Maxime Dénès
charguer
Matthieu Sozeau
Thomas Hebb
Vincent Laporte
Théo Zimmermann