aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
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-22Merge PR #9062: Delay the computation of frozen evars in legacy unification.Matthieu Sozeau
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-17Delay the computation of frozen evars in legacy unification.Pierre-Marie Pédrot
2019-08-16Split the [check_guarded] typing_flag into [check_guarded] (for (co)fixpoints...SimonBoulier
2019-08-16Merge PR #10457: Make rewrite use the registered elimination schemesPierre-Marie Pédrot
2019-08-10Make rewrite use the registered elimination schemesAndreas Lynge
2019-08-08Emit Feedback.AddedAxiom in Declare instead of higher layersGaëtan Gilbert
2019-08-07Merge PR #10604: Simplify Lib section handlingEmilio Jesus Gallego Arias
2019-07-31Specialize the section API.Pierre-Marie Pédrot
2019-07-31Remove the universe part from the section variable mechanism.Pierre-Marie Pédrot
2019-07-31[funind] Port aux function to the new tactic engine.Emilio Jesus Gallego Arias
2019-07-11Merge PR #10498: [api] Deprecate GlobRef constructors.Gaëtan Gilbert
2019-07-11Merge PR #10439: Uniform handling of side-effects for opaque definitionsMaxime Dénès
2019-07-08Similar purity invariants in the kernel.Pierre-Marie Pédrot
2019-07-08Further cleanup following the removal of pure opaque definitions.Pierre-Marie Pédrot
2019-07-08Do not export side-effects of polymorphic definitions.Pierre-Marie Pédrot
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-07-08[core] [api] Support OCaml 4.08Emilio Jesus Gallego Arias
2019-07-03declare_variable: path is always Lib.cwd()Gaëtan Gilbert
2019-07-03Remove unused Decls.variable_{context,polymorphic}Gaëtan Gilbert
2019-07-03Declare section variables in direct style "without" an objectGaëtan Gilbert
2019-07-03Move declare_universe_context to top of DeclareGaëtan Gilbert
2019-07-03Safe_typing.push_named_assum: don't take universesGaëtan Gilbert
2019-07-03Simplify (restrict_path 0 sp) -> (make_path DirPath.empty id)Gaëtan Gilbert
2019-07-02[declare] Cleanup on imports, move exception.Emilio Jesus Gallego Arias
2019-07-01[declare] Remove superfluous APIEmilio Jesus Gallego Arias
2019-07-01[declare] Separate kinds from entries in constant declarationEmilio Jesus Gallego Arias
2019-07-01[dumpglob] Move dumpglob-specific data to dumpglob.Emilio Jesus Gallego Arias
2019-07-01[api] Refactor most of `Decl_kinds`Emilio Jesus Gallego Arias
2019-06-27Kernel transparent definition entries have no body universes.Gaëtan Gilbert
2019-06-26Perform the opaque section variable inference outside of the kernel.Pierre-Marie Pédrot
2019-06-25Move the internal_flag type from Declare to Ind_tables.Pierre-Marie Pédrot
2019-06-25Remove the internal_flag argument from Declare API.Pierre-Marie Pédrot
2019-06-25Make dependence in Declare explicit in tactics.Pierre-Marie Pédrot
2019-06-24Use named records instead of tuples where `polymorphic` used to be.Gaëtan Gilbert
2019-06-24[api] Remove `polymorphic` type alias, use labels instead.Emilio Jesus Gallego Arias
2019-06-24[api] Move `locality` from `library` to `vernac`.Emilio Jesus Gallego Arias
2019-06-24[lemmas] [proof] Split proof kinds into per-layer components.Emilio Jesus Gallego Arias
2019-06-24[proof] Remove duplicated universe polymorphic from decl_kindsEmilio Jesus Gallego Arias
2019-06-24Remove the export_seff flag from Declare API.Pierre-Marie Pédrot
2019-06-24Remove the unused opaque_entry_inline_code field from opaque entries.Pierre-Marie Pédrot
2019-06-24Enforce that opaque entries carry their type.Pierre-Marie Pédrot
2019-06-24Dedicated type for opaque entries in the kernel.Pierre-Marie Pédrot
2019-06-24Enforce that transparent entries are forced beforehand.Pierre-Marie Pédrot
2019-06-24Take advantage of the change of entry representation to split opacity status.Pierre-Marie Pédrot
2019-06-24Duplicate the type of constant entries in Proof_global.Pierre-Marie Pédrot
2019-06-24Move Declare to tactics folder.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 06:12:26 +0000