index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2020-07-12
Adding change log.
Hugo Herbelin
2020-07-12
Fixes #12682 (recursive notation printing bug with n-ary applications).
Hugo Herbelin
2020-07-11
tactics.rst: `Require A` is enough for `A`'s hints
Paolo G. Giarrusso
2020-07-11
Merge PR #12650: Recordops: unify struc_typ summary record and libobject entr...
Pierre-Marie Pédrot
2020-07-11
Merge PR #12646: Correctly readback blocked CaseInvert matches in VM/native
Pierre-Marie Pédrot
2020-07-11
Merge PR #12635: Correct comment and clarify constant
Pierre-Marie Pédrot
2020-07-10
Merge PR #12638: Some changes of representation in Tacred
Enrico Tassi
2020-07-10
Add changelog.
Pierre-Marie Pédrot
2020-07-10
Fix #12513: coq no longer reports mismatched version numbers.
Pierre-Marie Pédrot
2020-07-10
Minor improvement to CI logs
Gaëtan Gilbert
2020-07-10
Merge PR #12666: Add test for #10890 derive vs abstract
Emilio Jesus Gallego Arias
2020-07-10
Fix fiat_crypto(_ocaml) needs/dependencies
Gaëtan Gilbert
2020-07-10
Merge PR #12537: Take into account the existing delta-resolver when starting ...
Gaëtan Gilbert
2020-07-09
Merge PR #12542: Defined arbitrary base logarithms (Rlog) and added natural l...
Michael Soegtrop
2020-07-09
[error handling] Anomaly in Conversion is a "precatchable_exception"
Emilio Jesus Gallego Arias
2020-07-09
[reductionops] Comment about absorption of anomalies.
Emilio Jesus Gallego Arias
2020-07-09
[exn] Remove some uses of print
Emilio Jesus Gallego Arias
2020-07-09
Add test for #10890 derive vs abstract
Gaëtan Gilbert
2020-07-09
Overlay for removing struc_tuple
Gaëtan Gilbert
2020-07-09
Recordops: unify struc_typ summary record and libobject entry struc_tuple
Gaëtan Gilbert
2020-07-09
Merge PR #11836: [obligations] Functionalize Program state
Gaëtan Gilbert
2020-07-09
Fix typo in contributing guide.
Théo Zimmermann
2020-07-08
Add tags in prodn indicating productions that are from plugins,
Jim Fehrle
2020-07-08
Make local nonterminal definitions unique when necessary
Jim Fehrle
2020-07-08
Merge PR #12627: Fix Canonical with universe polymorphism and primitive proje...
Enrico Tassi
2020-07-08
declare: Add [save_regular] API for obligation-ignoring proofs
Gaëtan Gilbert
2020-07-08
[ci] Overlay for metacoq and rewriter
Emilio Jesus Gallego Arias
2020-07-08
[declare] Allow obligations update on equations closing hook.
Emilio Jesus Gallego Arias
2020-07-08
[obligations] Allow to simultaneously open a proof and add obligations
Emilio Jesus Gallego Arias
2020-07-08
[obligations] Allow state-modifying hooks
Emilio Jesus Gallego Arias
2020-07-08
[obligations] Remove duplicate progmap_remove.
Emilio Jesus Gallego Arias
2020-07-08
[obligations] Functionalize Program state
Emilio Jesus Gallego Arias
2020-07-08
[declare] Generalize type of hooks.
Emilio Jesus Gallego Arias
2020-07-08
Adding change log.
Hugo Herbelin
2020-07-08
Adding test for #12525 (Search of lemmas in Include failing when in Module).
Hugo Herbelin
2020-07-08
Merge PR #12612: docs(README.md): Update badge and links
Emilio Jesus Gallego Arias
2020-07-08
Merge PR #12654: Reindent ppvernac.ml
Emilio Jesus Gallego Arias
2020-07-08
Merge PR #12645: Cleanup Evarutil API
Emilio Jesus Gallego Arias
2020-07-08
Merge PR #12652: Fix erroneous implicits-in-term warning
Emilio Jesus Gallego Arias
2020-07-08
Preserve delta-resolver at Module and Module Type starting.
Hugo Herbelin
2020-07-08
Remove Evarutil.new_evar_instance from the API.
Pierre-Marie Pédrot
2020-07-08
Remove Evarutil.new_evar_from_context from the API.
Pierre-Marie Pédrot
2020-07-08
Remove Evarutil.new_pure_evar_full from the API.
Pierre-Marie Pédrot
2020-07-08
Small code simplification in Evarutil.new_evar.
Pierre-Marie Pédrot
2020-07-07
Merge PR #12626: Fix Context with nonmaximplicit.
Emilio Jesus Gallego Arias
2020-07-07
Reindent ppvernac.ml
Gaëtan Gilbert
2020-07-07
Fix erroneous implicits-in-term warning
Gaëtan Gilbert
2020-07-06
Merge PR #11604: Primitive persistent arrays
Pierre-Marie Pédrot
2020-07-06
Correctly readback blocked CaseInvert matches in VM/native
Gaëtan Gilbert
2020-07-06
Primitive persistent arrays
Maxime Dénès
[prev]
[next]