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
*
Simplification: cumulativity information is variance information.
Gaëtan Gilbert
2018-02-10
*
[get_cumulativity_constraints] allowing further code sharing.
Gaëtan Gilbert
2018-02-10
*
Factorize code for comparing maybe-cumulative inductives.
Gaëtan Gilbert
2018-02-10
*
Fix typo in Univ.CumulativityInfo
Gaëtan Gilbert
2018-02-10
*
Merge PR #6657: Document the Fail command
Maxime Dénès
2018-02-07
|
\
*
\
Merge PR #6685: Use whd-all on rigid-flex conversion.
Maxime Dénès
2018-02-07
|
\
\
*
\
\
Merge PR #6610: Points to Flocq official repository.
Maxime Dénès
2018-02-07
|
\
\
\
*
\
\
\
Merge PR #6686: Kernel/checker reduction cleanups around projection unfolding
Maxime Dénès
2018-02-07
|
\
\
\
\
*
\
\
\
\
Merge PR #6673: Fix evar handling in native_compute conversion
Maxime Dénès
2018-02-07
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #6671: [stm] [toplevel] Make loadpath a parameter of the document.
Maxime Dénès
2018-02-06
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #6695: [toplevel] Refine start of interactive mode conditions.
Maxime Dénès
2018-02-06
|
\
\
\
\
\
\
\
|
|
|
|
|
*
|
|
Points to Flocq official repository.
Théo Zimmermann
2018-02-05
|
|
_
|
_
|
_
|
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
*
|
Respect the transparent state of the current conversion on strong weak-head.
Pierre-Marie Pédrot
2018-02-05
|
|
|
|
*
|
|
Add overlay for equations (nf_beta takes an env)
Gaëtan Gilbert
2018-02-05
|
|
|
*
|
|
|
[native_compute] Fix handling of evars in conversion
Maxime Dénès
2018-02-05
|
|
|
*
|
|
|
[native_compute] Remove useless conversion to list in reification.
Maxime Dénès
2018-02-05
|
|
_
|
/
/
/
/
|
/
|
|
|
|
|
*
|
|
|
|
|
Merge PR #6653: [vernac] Remove VernacGoal, allow anonymous definitions in Ve...
Maxime Dénès
2018-02-05
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #6654: CI: Run coqchk on Iris
Maxime Dénès
2018-02-05
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #6652: Allow vernacular controls before focus selector
Maxime Dénès
2018-02-05
|
\
\
\
\
\
\
\
\
|
|
|
|
|
*
|
|
|
[stm] [toplevel] Make loadpath a parameter of the document.
Emilio Jesus Gallego Arias
2018-02-05
|
|
|
|
|
/
/
/
/
|
|
|
|
*
/
/
/
[toplevel] Refine start of interactive mode conditions.
Emilio Jesus Gallego Arias
2018-02-05
|
|
_
|
_
|
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
*
|
|
CClosure.unfold_projection: don't catch Not_found, assume env is ok
Gaëtan Gilbert
2018-02-02
|
|
|
|
*
|
|
Reductionops.nf_* now take an environment.
Gaëtan Gilbert
2018-02-02
|
|
|
|
*
|
|
checker: cleanup projection unfolding
Gaëtan Gilbert
2018-02-02
|
|
|
|
*
|
|
checker: remove unused per-constant reduction flags.
Gaëtan Gilbert
2018-02-02
|
|
|
|
*
|
|
kernel: cleanup projection unfolding
Gaëtan Gilbert
2018-02-02
|
|
_
|
_
|
/
/
/
|
/
|
|
|
|
|
|
|
|
|
*
|
Use whd-all on rigid-flex conversion.
Pierre-Marie Pédrot
2018-02-02
|
|
_
|
_
|
/
/
|
/
|
|
|
|
*
|
|
|
|
Merge PR #6670: Delete duplicate line
Maxime Dénès
2018-02-01
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #6675: [proofview] enter_one: add __LOC__ argument to get relevant e...
Maxime Dénès
2018-02-01
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #6672: [stm] Move options to a per-document record.
Maxime Dénès
2018-02-01
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #6660: [lib] Respect change of options under with/without_option.
Maxime Dénès
2018-02-01
|
\
\
\
\
\
\
\
\
|
|
|
|
|
|
|
*
|
[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
|
|
_
|
_
|
_
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
*
|
CI: Run coqchk on Iris
Ralf Jung
2018-01-31
|
|
|
*
|
|
|
|
Proofview: enter_one: add __LOC__ argument to get relevant error msg
Enrico Tassi
2018-01-31
|
|
*
|
|
|
|
|
[stm] Move options to a per-document record.
Emilio Jesus Gallego Arias
2018-01-31
|
|
/
/
/
/
/
/
|
/
|
|
|
|
|
|
*
|
|
|
|
|
|
Merge PR #6601: Circle CI: fix cache selection.
Maxime Dénès
2018-01-31
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #6641: ci-compcert.sh: use default value for NJOBS when installing m...
Maxime Dénès
2018-01-31
|
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
Merge PR #6663: [toplevel] Refactor load path handling.
Maxime Dénès
2018-01-31
|
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
Merge PR #6656: Fix #5747: "make validate" fails with "bad recursive trees"
Maxime Dénès
2018-01-31
|
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
Merge PR #6535: Cleanup name-binding structure for fresh evar name generation.
Maxime Dénès
2018-01-31
|
\
\
\
\
\
\
\
\
\
\
\
|
|
|
|
|
|
|
|
*
|
|
|
Delete duplicate line
Paul Steckler
2018-01-30
|
|
_
|
_
|
_
|
_
|
_
|
_
|
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
[lib] Respect change of options under with/without_option.
Emilio Jesus Gallego Arias
2018-01-30
|
|
_
|
_
|
_
|
_
|
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
Put default value for NJOBS in ci-common.
Gaëtan Gilbert
2018-01-30
|
*
|
|
|
|
|
|
|
|
Adding an overlay for Equations.
Pierre-Marie Pédrot
2018-01-30
*
|
|
|
|
|
|
|
|
|
Merge PR #6666: Fix reduction of primitive projections on coinductive records...
Maxime Dénès
2018-01-30
|
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
Merge PR #6649: Fix #6621: Anomaly on fixpoint with primitive projections
Maxime Dénès
2018-01-30
|
\
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
\
Merge PR #6636: Stop running duplicate Travis jobs on pull requests.
Maxime Dénès
2018-01-30
|
\
\
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
\
\
Merge PR #6605: Safer VM interfaces
Maxime Dénès
2018-01-30
|
\
\
\
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
\
\
\
Merge PR #6644: Use travis_retry on apt-get update
Maxime Dénès
2018-01-30
|
\
\
\
\
\
\
\
\
\
\
\
\
\
\
|
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
[next]