aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2020-01-30Merge PR #11307: Remove the hacks relying on hardwired libobject tags.Maxime Dénès
2020-01-27schemes: use rigid universesGaëtan Gilbert
2020-01-21Translating a comment from French to English.Hugo Herbelin
2020-01-12fix #11279. Specialize h no longer expands letins in the type of h.Pierre Courtieu
2019-12-22Remove the hacks relying on hardwired libobject tags.Pierre-Marie Pédrot
2019-12-18Merge PR #10616: Fix push_universe_context* interfaces to use a consistent ~s...Pierre-Marie Pédrot
2019-12-16Pretyping.check_evars: make initial evar map optionalGaëtan Gilbert
2019-12-13Use ~strict argument consistently in push_context/push_context_set intfsMatthieu Sozeau
2019-12-11Merge PR #11271: Fixing #9893. "Specialize with" would not support hyps type ...Pierre-Marie Pédrot
2019-12-10Fixing #9893 (Letins not supported in the specialized hypothesis).Pierre Courtieu
2019-12-10Side-effect free wrapper around already declared schemes.Pierre-Marie Pédrot
2019-12-10Make explicit that users should not observe return values of scheme functions.Pierre-Marie Pédrot
2019-12-10Simplify internal flags in scheme declarations.Pierre-Marie Pédrot
2019-12-06Moving the diversity of constr printers to a label style.Hugo Herbelin
2019-11-30Actually deprecate the `cutrewrite` tacticMaxime Dénès
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-11Do not export the internals of the prepare_hint function.Pierre-Marie Pédrot
2019-11-08Make [Proof_global.closed_proof_output] opaqueGaëtan Gilbert
2019-11-01Add primitive float computation in Coq kernelGuillaume Bertholon
2019-10-30[declare] Remove declare_scheme hook in DeclareEmilio Jesus Gallego Arias
2019-10-30Merge PR #10981: [abstract] Remove un-unused reference to `evar_map`Pierre-Marie Pédrot
2019-10-30Merge PR #10949: [declare] Provide helper for private constant inlining.Pierre-Marie Pédrot
2019-10-30Merge PR #10681: [declare] Make `proof_entry` a private type.Pierre-Marie Pédrot
2019-10-30Merge PR #10494: Show diffs in "Show Proof."Enrico Tassi
2019-10-29Show diffs in "Show Proof."Jim Fehrle
2019-10-29[abstract] Remove un-unused reference to `evar_map`Emilio Jesus Gallego Arias
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 #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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 10:44:51 +0000