aboutsummaryrefslogtreecommitdiff
path: root/vernac/declare.ml
AgeCommit message (Expand)Author
2020-11-20[stm] [declare] Remove pinfo internals hack.Emilio Jesus Gallego Arias
2020-11-20[stm] [declare] Try to propagate safe bits of proof informationEmilio Jesus Gallego Arias
2020-11-12Merge PR #13289: Cosmetic cleaning of uState.ml: a bit of doc, more unity in ...Pierre-Marie Pédrot
2020-11-09[obligation] Proper handle no obligations on `Next Obligation`Emilio Jesus Gallego Arias
2020-11-04Cosmetic cleaning of uState.ml and related: a bit of doc, more unity in naming.Hugo Herbelin
2020-11-02attribute #[using] for Definition and FixpointEnrico Tassi
2020-10-27Merge PR #13075: Introducing the foundations for a name-alias-agnostic APIcoqbot-app[bot]
2020-10-23[declare] Remove recursive declaration from non-recursive functionsEmilio Jesus Gallego Arias
2020-10-21Deprecate the non-qualified equality functions on kerpairs.Pierre-Marie Pédrot
2020-10-15[declare] Fix types of mutual lemmas when using Admitted.Emilio Jesus Gallego Arias
2020-09-30Reimplement Admit Obligations using standard Admitted codeGaëtan Gilbert
2020-09-01Unify the shelvesMaxime Dénès
2020-09-01Merge PR #12892: Update update_global_env usagePierre-Marie Pédrot
2020-08-31[declare] Return both declared constants in Derive path.Emilio Jesus Gallego Arias
2020-08-31Update update_global_env usageGaëtan Gilbert
2020-08-24Update sigma instead of erasing it in `update_global_env`Maxime Dénès
2020-08-20[vernac] refine check for unresolved evarsEnrico Tassi
2020-07-20[declare] Remove some dead code in declare_mutual_definitionEmilio Jesus Gallego Arias
2020-07-15[search] Don't use ad-hoc Dumpglob table for SearchEmilio Jesus Gallego Arias
2020-07-08declare: Add [save_regular] API for obligation-ignoring proofsGaëtan Gilbert
2020-07-08[declare] Allow obligations update on equations closing hook.Emilio 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-06-29Move the FailError exception from Refiner to Tacticals.Pierre-Marie Pédrot
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[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[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] [compat] Remove exception alias.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 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 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-11[declare] Remove some unused `fix_exn`Emilio Jesus Gallego Arias
2020-06-08Don't suggest Proof using when no section variablesGaëtan Gilbert
2020-06-03[declare] Hide internals of variable declaration entries.Emilio Jesus Gallego Arias
2020-05-26[declare] Split univs_poly_private in close_proofEmilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:26:22 +0000