aboutsummaryrefslogtreecommitdiff
AgeCommit 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.saveEmilio 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 APIEmilio Jesus Gallego Arias
2020-06-26[declare] Merge remaining obligations bits into DeclareEmilio Jesus Gallego Arias
2020-06-26[obligation] Switch to new declare info API.Emilio Jesus Gallego Arias
2020-06-26[declare] Improve logical code orderEmilio 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 interpretationEmilio 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 functionsEmilio Jesus Gallego Arias
2020-06-26[declare] Refactor analysis and construction of mutual lemmasEmilio Jesus Gallego Arias
2020-06-26[declare] Nit on hook call.Emilio Jesus Gallego Arias
2020-06-26[declare] Nit on interfaceEmilio Jesus Gallego Arias
2020-06-26[declare] Documentation on obligationsEmilio 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 interfacesEmilio 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 functionsEmilio Jesus Gallego Arias
2020-06-26[declare] Make ProgramDecl.t abstractEmilio Jesus Gallego Arias
2020-06-26[declare] Refactor constant information into a record.Emilio Jesus Gallego Arias
2020-06-26[declare] Remove Lemmas moduleEmilio 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_proofEmilio Jesus Gallego Arias
2020-06-26Credit Erik Martin-Dorel for work on Docker.Théo Zimmermann
2020-06-25Merge PR #12554: Add back fiat-crypto-legacy to the CIEmilio Jesus Gallego Arias
2020-06-25Merge PR #12579: Simplify Clenv APIEmilio Jesus Gallego Arias
2020-06-25Merge PR #12580: Remove the catchable-exception related functions.Emilio Jesus Gallego Arias
2020-06-25[ci] [ocaml] Track OCaml 4.12Emilio Jesus Gallego Arias
2020-06-25Generate names for anonymous polymorphic universesGaëtan Gilbert
2020-06-25Make compute_instance_binders internal to UStateGaëtan Gilbert
2020-06-24[ci] [fiat-crypto-legacy] allow_failure: trueJason Gross
2020-06-24[test-suite] Fix dependencies of modules/ filesJason Gross
2020-06-24Merge PR #12517: Fix #4459 by improving `par:` error messageEnrico Tassi
2020-06-24Add back fiat-crypto-legacy to the CIJason Gross
2020-06-24Remove the catchable-exception related functions.Pierre-Marie Pédrot
2020-06-24Simplify Clenv.clenv_pose_metas_as_evars.Pierre-Marie Pédrot
2020-06-24Actually remove internal API from the Clenv mli.Pierre-Marie Pédrot
2020-06-24Merge Clenvtac into Clenv.Pierre-Marie Pédrot
2020-06-24Remove all uses of clenv_unique_resolver.Pierre-Marie Pédrot
2020-06-24Remove dead code in branch_args.Pierre-Marie Pédrot
2020-06-24Merge PR #12550: Fix configure usage in .opamEmilio Jesus Gallego Arias
2020-06-24Merge PR #12532: Use the unification result for eauto's eapply.Matthieu Sozeau
2020-06-24Revert "[opam] Don't disable native compute in opam.dev file"Gaëtan Gilbert
2020-06-24Merge PR #12577: [ci] Add coq-community/coq-performance-testsGaëtan Gilbert
2020-06-23[ci] Add coq-community/coq-performance-testsJason Gross
2020-06-23Correctly classify variables as being unfoldable in dnet patterns.Pierre-Marie Pédrot