aboutsummaryrefslogtreecommitdiff
path: root/tactics/declare.ml
AgeCommit message (Expand)Author
2020-04-15[declare] Rename `Declare.t` to `Declare.Proof.t`Emilio Jesus Gallego Arias
2020-04-15[proof] Move functions related to `Proof.t` to `Proof`Emilio Jesus Gallego Arias
2020-04-15[proof] Merge `Pfedit` into proofs.Emilio Jesus Gallego Arias
2020-04-15[declare] [abstract] Do evars check in declare_abstractEmilio Jesus Gallego Arias
2020-04-15[declare] Mark APIs as scheduled for removal; remove a couple.Emilio Jesus Gallego Arias
2020-04-15[proof] [abstract] Move internal declaration code to `Declare`Emilio Jesus Gallego Arias
2020-04-15[proof] Merge `Proof_global` into `Declare`Emilio Jesus Gallego Arias
2020-04-13correctly open objects for Names filtersGaëtan Gilbert
2020-04-13pass filters aroundGaëtan Gilbert
2020-03-31[proof] Improve comment and argument name.Emilio Jesus Gallego Arias
2020-03-31[proof] Split delayed and regular proof closing functions, part IIEmilio Jesus Gallego Arias
2020-03-19[declare] Remaining bits on the consistency of UState.t namingEmilio Jesus Gallego Arias
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-24[exn] Forbid raising in exn printers, make them return Pp.t optionEmilio Jesus Gallego Arias
2020-01-30Factorize export_private_constants + register_side_effectGaëtan Gilbert
2020-01-30export_private_constants doesn't use the [constr in_univ_ctx] argumentGaëtan Gilbert
2020-01-30Merge PR #11307: Remove the hacks relying on hardwired libobject tags.Maxime Dénès
2020-01-21Translating a comment from French to English.Hugo Herbelin
2019-12-22Remove the hacks relying on hardwired libobject tags.Pierre-Marie Pédrot
2019-12-13Use ~strict argument consistently in push_context/push_context_set intfsMatthieu Sozeau
2019-10-30[declare] Remove declare_scheme hook in DeclareEmilio Jesus Gallego Arias
2019-10-30Merge PR #10949: [declare] Provide helper for private constant inlining.Pierre-Marie Pédrot
2019-10-29[declare] Use helper function for `fix_exn` instead of relying on internals.Emilio Jesus Gallego Arias
2019-10-29[declare] Make `proof_entry` a private type.Emilio Jesus Gallego Arias
2019-10-28[declare] Provide helper for private constant inlining.Emilio Jesus Gallego Arias
2019-10-24[declare] Split inductive declaration code to vernac/Emilio Jesus Gallego Arias
2019-10-24[declare] Split universe declaration code to vernac/Emilio Jesus Gallego Arias
2019-10-16Simplify future forcing in Declare.Pierre-Marie Pédrot
2019-10-16Ensure that side-effect declarations reaching the kernel are forced.Pierre-Marie Pédrot
2019-10-16Split the function used to declare side-effects from the standard one.Pierre-Marie Pédrot
2019-10-16Cleaning up the previous code by ensuring statically invariants on opaque pro...Pierre-Marie Pédrot
2019-10-14Use kernel info from Global for Lib.sections_{depth,are_opened}Gaëtan Gilbert
2019-10-14Remove [in_section] arguments to Safe_typing functionsGaëtan Gilbert
2019-10-13Merge PR #10670: ComAssumption cleanupPierre-Marie Pédrot
2019-10-11Merge PR #10804: Fix Print All of section variablesPierre-Marie Pédrot
2019-10-05Remove "is_polymorphic_univ" checks in upper layers.Gaëtan Gilbert
2019-10-05Declare universes for variables outside of Declare.declare_variableGaëtan Gilbert
2019-10-04Remove redundancy in section hypotheses of kernel entries.Pierre-Marie Pédrot
2019-10-01Fix Print All of section variablesGaëtan Gilbert
2019-09-28Remove the monomorphic universe libobject.Pierre-Marie Pédrot
2019-09-26Implement section discharging inside kernel.Pierre-Marie Pédrot
2019-09-25Move the Lib section data into the kernel.Pierre-Marie Pédrot
2019-09-25Refine the API to declare section-local universes.Pierre-Marie Pédrot
2019-08-29Merge PR #10674: [declare] Move proof_entry type to declare, put interactive ...Pierre-Marie Pédrot
2019-08-27[declare] Move proof_entry type to declare, put interactive proof data on top...Emilio Jesus Gallego Arias
2019-08-26[glob/aux files] Remove undocumented Stdout dump, cleanup flags.Emilio Jesus Gallego Arias
2019-08-23Merge PR #10665: [api] Move handling of variable implicit data to impargsGaëtan Gilbert
2019-08-19[declare] Use `binding_kind` for implicit kind instead of boolean.Emilio Jesus Gallego Arias
2019-08-19[api] Move handling of variable implicit data to impargsEmilio Jesus Gallego Arias
2019-08-16Split the [check_guarded] typing_flag into [check_guarded] (for (co)fixpoints...SimonBoulier
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-22 03:44:02 +0000