aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-07-12Adding change log.Hugo Herbelin
2020-07-12Fixes #12682 (recursive notation printing bug with n-ary applications).Hugo Herbelin
2020-07-11tactics.rst: `Require A` is enough for `A`'s hintsPaolo G. Giarrusso
2020-07-11Merge PR #12650: Recordops: unify struc_typ summary record and libobject entr...Pierre-Marie Pédrot
2020-07-11Merge PR #12646: Correctly readback blocked CaseInvert matches in VM/nativePierre-Marie Pédrot
2020-07-11Merge PR #12635: Correct comment and clarify constantPierre-Marie Pédrot
2020-07-10Merge PR #12638: Some changes of representation in TacredEnrico Tassi
2020-07-10Add changelog.Pierre-Marie Pédrot
2020-07-10Fix #12513: coq no longer reports mismatched version numbers.Pierre-Marie Pédrot
2020-07-10Minor improvement to CI logsGaëtan Gilbert
2020-07-10Merge PR #12666: Add test for #10890 derive vs abstractEmilio Jesus Gallego Arias
2020-07-10Fix fiat_crypto(_ocaml) needs/dependenciesGaëtan Gilbert
2020-07-10Merge PR #12537: Take into account the existing delta-resolver when starting ...Gaëtan Gilbert
2020-07-09Merge 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 printEmilio Jesus Gallego Arias
2020-07-09Add test for #10890 derive vs abstractGaëtan Gilbert
2020-07-09Overlay for removing struc_tupleGaëtan Gilbert
2020-07-09Recordops: unify struc_typ summary record and libobject entry struc_tupleGaëtan Gilbert
2020-07-09Merge PR #11836: [obligations] Functionalize Program stateGaëtan Gilbert
2020-07-09Fix typo in contributing guide.Théo Zimmermann
2020-07-08Add tags in prodn indicating productions that are from plugins,Jim Fehrle
2020-07-08Make local nonterminal definitions unique when necessaryJim Fehrle
2020-07-08Merge PR #12627: Fix Canonical with universe polymorphism and primitive proje...Enrico Tassi
2020-07-08declare: Add [save_regular] API for obligation-ignoring proofsGaëtan Gilbert
2020-07-08[ci] Overlay for metacoq and rewriterEmilio 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 obligationsEmilio Jesus Gallego Arias
2020-07-08[obligations] Allow state-modifying hooksEmilio Jesus Gallego Arias
2020-07-08[obligations] Remove duplicate progmap_remove.Emilio Jesus Gallego Arias
2020-07-08[obligations] Functionalize Program stateEmilio Jesus Gallego Arias
2020-07-08[declare] Generalize type of hooks.Emilio Jesus Gallego Arias
2020-07-08Adding change log.Hugo Herbelin
2020-07-08Adding test for #12525 (Search of lemmas in Include failing when in Module).Hugo Herbelin
2020-07-08Merge PR #12612: docs(README.md): Update badge and linksEmilio Jesus Gallego Arias
2020-07-08Merge PR #12654: Reindent ppvernac.mlEmilio Jesus Gallego Arias
2020-07-08Merge PR #12645: Cleanup Evarutil APIEmilio Jesus Gallego Arias
2020-07-08Merge PR #12652: Fix erroneous implicits-in-term warningEmilio Jesus Gallego Arias
2020-07-08Preserve delta-resolver at Module and Module Type starting.Hugo Herbelin
2020-07-08Remove Evarutil.new_evar_instance from the API.Pierre-Marie Pédrot
2020-07-08Remove Evarutil.new_evar_from_context from the API.Pierre-Marie Pédrot
2020-07-08Remove Evarutil.new_pure_evar_full from the API.Pierre-Marie Pédrot
2020-07-08Small code simplification in Evarutil.new_evar.Pierre-Marie Pédrot
2020-07-07Merge PR #12626: Fix Context with nonmaximplicit.Emilio Jesus Gallego Arias
2020-07-07Reindent ppvernac.mlGaëtan Gilbert
2020-07-07Fix erroneous implicits-in-term warningGaëtan Gilbert
2020-07-06Merge PR #11604: Primitive persistent arraysPierre-Marie Pédrot
2020-07-06Correctly readback blocked CaseInvert matches in VM/nativeGaëtan Gilbert
2020-07-06Primitive persistent arraysMaxime Dénès