aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2020-07-01[state] Consolidate state handling in VernacstateEmilio Jesus Gallego Arias
2020-07-01UIP in SPropGaëtan Gilbert
2020-07-01Merge PR #12504: [states] Move States to vernacGaëtan Gilbert
2020-06-30Merge PR #12599: Remove the Refiner moduleEmilio Jesus Gallego Arias
2020-06-30[declaremods] Remove abstraction of imperative module operationsEmilio Jesus Gallego Arias
2020-06-30[states] Move States to vernacEmilio Jesus Gallego Arias
2020-06-30Merge PR #11977: Generate default names for bound universes of polymorphic de...Emilio Jesus Gallego Arias
2020-06-29Move the FailError exception from Refiner to Tacticals.Pierre-Marie Pédrot
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-25Generate names for anonymous polymorphic universesGaëtan Gilbert
2020-06-19Merge PR #12531: Fast inductive compilationGaëtan Gilbert
2020-06-17Check duplicity of constructor names in an algorithmically efficient way.Pierre-Marie Pédrot
2020-06-13[toplevel] Annotate tailcall functionsEmilio Jesus Gallego Arias
2020-06-11[declare] Remove some unused `fix_exn`Emilio Jesus Gallego Arias
2020-06-08Merge PR #12480: Don't suggest Proof using when no section variablesEmilio Jesus Gallego Arias
2020-06-08Don't suggest Proof using when no section variablesGaëtan Gilbert
2020-06-06Fix uncaught NotArity in inductive typeGaëtan Gilbert
2020-06-03[declare] Hide internals of variable declaration entries.Emilio Jesus Gallego Arias
2020-06-02Merge PR #11974: Require in Section: warning is now about fragility not depre...Emilio Jesus Gallego Arias
2020-05-29Merge PR #12393: [declare] Miscellaneous nits from my main dev treeGaëtan Gilbert
2020-05-29Require in Section: warning is now about fragility not deprecation.Gaëtan Gilbert
2020-05-28Fixing compilation with -natdynlink no.Hugo Herbelin
2020-05-26[declare] Split univs_poly_private in close_proofEmilio Jesus Gallego Arias
2020-05-26[declare] Factor common universe computation in close proof.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 04:19:10 +0000