index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.
Hugo Herbelin
2018-02-20
*
Rephrasing ETBinderList with a self-documenting and invariant-carrying argument.
Hugo Herbelin
2018-02-20
*
Notations: Do not consider a non-occurring variable as a binder-only variable.
Hugo Herbelin
2018-02-20
*
More precise explanation when a notation is not reversible for printing.
Hugo Herbelin
2018-02-20
*
Adding support for re-folding notation referring to isolated "forall '(x,y), t".
Hugo Herbelin
2018-02-20
*
Again one more step in fixing #5762 ("where" clause).
Hugo Herbelin
2018-02-20
*
Merge PR #6728: Extrude monomorphic universe contexts from with Definition co...
Maxime Dénès
2018-02-19
|
\
*
\
Merge PR #6761: Remove unused argument in Record.declare_structure
Maxime Dénès
2018-02-19
|
\
\
*
\
\
Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`
Maxime Dénès
2018-02-19
|
\
\
\
*
\
\
\
Merge PR #6753: [toplevel] Make toplevel state into a record.
Maxime Dénès
2018-02-19
|
\
\
\
\
*
\
\
\
\
Merge PR #6230: Better Cemitcodes API + compact relocation representation
Maxime Dénès
2018-02-19
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #6759: detype_case predicate is not optional
Maxime Dénès
2018-02-19
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #6772: Cleanup inferCumulativity
Maxime Dénès
2018-02-19
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #6648: [tactics] make apply_type safe
Maxime Dénès
2018-02-19
|
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ...
Maxime Dénès
2018-02-19
|
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead.
Maxime Dénès
2018-02-19
|
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
Merge PR #6478: [build] Fix VM dynamic linking prep in byte builds.
Maxime Dénès
2018-02-19
|
\
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
\
Merge PR #6571: Fix ci-all target
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
|
|
|
|
|
*
|
|
|
|
|
|
|
apply_type: add option "typecheck" passed down to refine
Enrico Tassi
2018-02-16
|
|
_
|
_
|
_
|
/
/
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
Cleaner treatment of parameters in inferCumulativity
Gaëtan Gilbert
2018-02-16
|
|
|
|
|
*
|
|
|
|
|
|
Fix reduction flags in inferCumulativity
Gaëtan Gilbert
2018-02-16
|
|
_
|
_
|
_
|
/
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*
Adding a test for the construction that was broken in Coccinelle.
Pierre-Marie Pédrot
2018-02-16
|
|
|
|
|
|
|
|
|
|
*
Extrude monomorphic universe contexts from with Definition constraints.
Pierre-Marie Pédrot
2018-02-16
|
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*
|
|
[toplevel] Make toplevel state into a record.
Emilio Jesus Gallego Arias
2018-02-15
|
|
|
|
|
|
|
*
|
|
[ide] Localize a IDE-specific flag.
Emilio Jesus Gallego Arias
2018-02-15
|
|
_
|
_
|
_
|
_
|
_
|
/
/
/
|
/
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
|
Merge PR #1073: new quick2vo target: like vio2vo, but smarter
Maxime Dénès
2018-02-15
|
\
\
\
\
\
\
\
\
\
|
*
|
|
|
|
|
|
|
|
disable tests: vio2vo is broken in Windows
Ralf Jung
2018-02-15
|
*
|
|
|
|
|
|
|
|
also test vio2vo
Ralf Jung
2018-02-15
|
*
|
|
|
|
|
|
|
|
test "make quick2vo"
Ralf Jung
2018-02-15
|
*
|
|
|
|
|
|
|
|
new quick2vo target: like vio2vo, but smarter
Ralf Jung
2018-02-15
|
|
|
_
|
_
|
/
/
/
/
/
|
|
/
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
|
Merge PR #6741: coq_makefile: Support "" as the prefix in _CoqProject
Maxime Dénès
2018-02-15
|
\
\
\
\
\
\
\
\
\
|
*
|
|
|
|
|
|
|
|
coq_makefile: Support "" as the prefix in _CoqProject
Joachim Breitner
2018-02-15
*
|
|
|
|
|
|
|
|
|
Merge PR #6760: CHANGES for 8.7.2.
Maxime Dénès
2018-02-15
|
\
\
\
\
\
\
\
\
\
\
|
*
|
|
|
|
|
|
|
|
|
CHANGES for 8.7.2.
Théo Zimmermann
2018-02-14
|
/
/
/
/
/
/
/
/
/
/
|
|
|
|
|
|
|
|
|
*
Remove unused argument in Record.declare_structure
Gaëtan Gilbert
2018-02-14
|
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*
|
Factorize the relocations in the on-disk VM representation.
Pierre-Marie Pédrot
2018-02-14
|
|
|
|
|
|
|
*
|
Use a more compact representation for bytecode relocations stored on disk.
Pierre-Marie Pédrot
2018-02-14
|
|
|
|
|
|
|
*
|
Do not use global variables for VM bytecode compilation in Cemitcodes.
Pierre-Marie Pédrot
2018-02-14
|
|
|
|
|
|
|
*
|
Remove the unsafe bytes conversion function in Cemitcodes.
Pierre-Marie Pédrot
2018-02-14
|
|
|
|
|
|
|
*
|
Move the call to the computation of bytecode inside Cemitcodes.
Pierre-Marie Pédrot
2018-02-14
|
|
|
|
|
|
|
*
|
Abstract further the type of VM bytecode compilation.
Pierre-Marie Pédrot
2018-02-14
|
|
_
|
_
|
_
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
*
|
detype_case predicate is not optional
Gaëtan Gilbert
2018-02-14
*
|
|
|
|
|
|
|
Merge PR #6742: Add CHANGES entry for #1047 (universe instance on Type notation)
Maxime Dénès
2018-02-14
|
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
Merge PR #6713: Fix #6677: Critical bug with VM and universes
Maxime Dénès
2018-02-14
|
\
\
\
\
\
\
\
\
\
|
|
|
|
|
|
*
|
|
|
[build] Fix VM dynamic linking prep in byte builds.
Emilio Jesus Gallego Arias
2018-02-14
|
|
|
|
|
_
|
/
/
/
/
|
|
|
|
/
|
|
|
|
|
|
|
|
|
|
|
*
|
|
coqdev.el: wait for 'compile to touch compilation-error-regexp-alist
Gaëtan Gilbert
2018-02-13
|
|
*
|
|
|
|
|
|
Add CHANGES entry for #1047
Tej Chajed
2018-02-13
|
|
|
/
/
/
/
/
/
|
|
|
|
|
*
|
|
coqdev.el: fix "compilate"-command typo
Gaëtan Gilbert
2018-02-13
|
|
|
|
|
*
|
|
coqdev.el: shell-quote-argument the directory for make -C
Gaëtan Gilbert
2018-02-13
[next]
Hugo Herbelin
Maxime Dénès
Jim Fehrle
Enrico Tassi
Gaëtan Gilbert
Pierre-Marie Pédrot
Emilio Jesus Gallego Arias
Ralf Jung
Joachim Breitner
Théo Zimmermann
Tej Chajed