aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
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 #10862: Simplify universe handling wrt side effects: rm demote_seff_...Pierre-Marie Pédrot
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-09Specialize UState.merge for extend:falseGaëtan Gilbert
2019-10-09Simplify universe handling wrt side effects: rm demote_seff_univsGaëtan Gilbert
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-09-04Merge PR #10612: Fix feedback levelsEmilio Jesus Gallego Arias
2019-08-30Merge PR #10714: Solve universe error with SSR 'rewrite !term'Pierre-Marie Pédrot
2019-08-29Solve universe error with SSR 'rewrite !term'Andreas Lynge
2019-08-29Merge PR #10674: [declare] Move proof_entry type to declare, put interactive ...Pierre-Marie Pédrot
2019-08-29Merge PR #10660: [cleanup] Replace uses of UserError constructor, clarify exc...Pierre-Marie Pédrot
2019-08-29Make sure that all query commands return a notice (not an info) feedbackMaxime Dénès
2019-08-27[declare] Use entry constructor instead of low-level record.Emilio Jesus Gallego Arias
2019-08-27[declare] Move proof_entry type to declare, put interactive proof data on top...Emilio Jesus Gallego Arias
2019-08-27[cleanup] Replace uses of UserError constructor, clarify exception names.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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:13:25 +0000