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-06-26
[recLemmas] Nit on naming consistency.
Emilio Jesus Gallego Arias
2020-06-26
[declare] Return list of declared global in Proof.save
Emilio Jesus Gallego Arias
2020-06-26
[declare] Some more cleanup on unused functions after the last commits.
Emilio Jesus Gallego Arias
2020-06-26
[declare] Remove Proof_ending from the public API
Emilio Jesus Gallego Arias
2020-06-26
[declare] Merge remaining obligations bits into Declare
Emilio Jesus Gallego Arias
2020-06-26
[obligation] Switch to new declare info API.
Emilio Jesus Gallego Arias
2020-06-26
[declare] Improve logical code order
Emilio Jesus Gallego Arias
2020-06-26
[declare] Improve organization of proof/constant information.
Emilio Jesus Gallego Arias
2020-06-26
[vernac] Nit refatoring on lemma command interpretation
Emilio Jesus Gallego Arias
2020-06-26
[declare] Nit on regular lemma init.
Emilio Jesus Gallego Arias
2020-06-26
[declare] Use Recthm.t in mutual analysis functions
Emilio Jesus Gallego Arias
2020-06-26
[declare] Refactor analysis and construction of mutual lemmas
Emilio Jesus Gallego Arias
2020-06-26
[declare] Nit on hook call.
Emilio Jesus Gallego Arias
2020-06-26
[declare] Nit on interface
Emilio Jesus Gallego Arias
2020-06-26
[declare] Documentation on obligations
Emilio Jesus Gallego Arias
2020-06-26
[declare] [compat] Remove exception alias.
Emilio Jesus Gallego Arias
2020-06-26
[declare] [api] Modify logical presentation of declare interfaces
Emilio Jesus Gallego Arias
2020-06-26
[declare] Reify Proof.t API into the Proof module.
Emilio Jesus Gallego Arias
2020-06-26
[declare] Move udecl to Info structure.
Emilio Jesus Gallego Arias
2020-06-26
[declare] [api] Removal of duplicated type aliases.
Emilio Jesus Gallego Arias
2020-06-26
[declare] [api] Removal of deprecated functions
Emilio Jesus Gallego Arias
2020-06-26
[declare] Make ProgramDecl.t abstract
Emilio Jesus Gallego Arias
2020-06-26
[declare] Refactor constant information into a record.
Emilio Jesus Gallego Arias
2020-06-26
[declare] Remove Lemmas module
Emilio Jesus Gallego Arias
2020-06-26
[declare] Remove mutual internals from Info.t structure.
Emilio Jesus Gallego Arias
2020-06-26
[declare] Move proof information to declare.
Emilio Jesus Gallego Arias
2020-06-26
[declare] Stronger typing for start_proof
Emilio Jesus Gallego Arias
2020-06-26
Credit Erik Martin-Dorel for work on Docker.
Théo Zimmermann
2020-06-25
Merge PR #12554: Add back fiat-crypto-legacy to the CI
Emilio Jesus Gallego Arias
2020-06-25
Merge PR #12579: Simplify Clenv API
Emilio Jesus Gallego Arias
2020-06-25
Merge PR #12580: Remove the catchable-exception related functions.
Emilio Jesus Gallego Arias
2020-06-25
[ci] [ocaml] Track OCaml 4.12
Emilio Jesus Gallego Arias
2020-06-25
Generate names for anonymous polymorphic universes
Gaëtan Gilbert
2020-06-25
Make compute_instance_binders internal to UState
Gaëtan Gilbert
2020-06-24
[ci] [fiat-crypto-legacy] allow_failure: true
Jason Gross
2020-06-24
[test-suite] Fix dependencies of modules/ files
Jason Gross
2020-06-24
Merge PR #12517: Fix #4459 by improving `par:` error message
Enrico Tassi
2020-06-24
Add back fiat-crypto-legacy to the CI
Jason Gross
2020-06-24
Remove the catchable-exception related functions.
Pierre-Marie Pédrot
2020-06-24
Simplify Clenv.clenv_pose_metas_as_evars.
Pierre-Marie Pédrot
2020-06-24
Actually remove internal API from the Clenv mli.
Pierre-Marie Pédrot
2020-06-24
Merge Clenvtac into Clenv.
Pierre-Marie Pédrot
2020-06-24
Remove all uses of clenv_unique_resolver.
Pierre-Marie Pédrot
2020-06-24
Remove dead code in branch_args.
Pierre-Marie Pédrot
2020-06-24
Merge PR #12550: Fix configure usage in .opam
Emilio Jesus Gallego Arias
2020-06-24
Merge PR #12532: Use the unification result for eauto's eapply.
Matthieu Sozeau
2020-06-24
Revert "[opam] Don't disable native compute in opam.dev file"
Gaëtan Gilbert
2020-06-24
Merge PR #12577: [ci] Add coq-community/coq-performance-tests
Gaëtan Gilbert
2020-06-23
[ci] Add coq-community/coq-performance-tests
Jason Gross
2020-06-23
Correctly classify variables as being unfoldable in dnet patterns.
Pierre-Marie Pédrot
[prev]
[next]