aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/rewrite.ml
AgeCommit message (Expand)Author
2021-03-30[flags] [profile] Remove bit-rotten CProfile code.Emilio Jesus Gallego Arias
2021-03-04Fix #12011 ssreflect "rewrite in" with setoidsGaëtan Gilbert
2021-01-04Change the representation of kernel case.Pierre-Marie Pédrot
2020-12-14Add checks for invalid occurrences in setoid rewrite.Hugo Herbelin
2020-11-18Merge PR #13341: Finish fixing setoid rewrite under anonymous lambdas (hopefu...Pierre-Marie Pédrot
2020-11-18Merge PR #13251: Make sure that setoid_rewrite passes state to subgoalsPierre-Marie Pédrot
2020-11-16Finish fixing setoid rewrite under anonymous lambdas (hopefully)Gaëtan Gilbert
2020-10-29Fixing interpretation of rewrite_strat argument in Ltac.Hugo Herbelin
2020-10-27Merge PR #13075: Introducing the foundations for a name-alias-agnostic APIcoqbot-app[bot]
2020-10-22Make sure that setoid_rewrite passes state to subgoalsLasse Blaauwbroek
2020-10-22Merge PR #13130: setoid_rewrite: record generated name when rewriting under l...Pierre-Marie Pédrot
2020-10-21Deprecate the non-qualified equality functions on kerpairs.Pierre-Marie Pédrot
2020-10-07Merge PR #13119: Fix retyping anomaly in rewritePierre-Marie Pédrot
2020-10-02setoid_rewrite: record generated name when rewriting under lambdaGaëtan Gilbert
2020-10-02Cleanup rewrite.mlGaëtan Gilbert
2020-09-30Fix retyping anomaly in rewriteGaëtan Gilbert
2020-09-30Further simplification of the typeclass registration API.Pierre-Marie Pédrot
2020-09-02Abstract type for allowed evarsMaxime Dénès
2020-09-02Replace `frozen` by `allowed` evars in evarconv, and delay themMaxime Dénès
2020-07-01UIP in SPropGaëtan Gilbert
2020-06-29Move the FailError exception from Refiner to Tacticals.Pierre-Marie Pédrot
2020-06-26[declare] Improve organization of proof/constant information.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] Refactor constant information into a record.Emilio Jesus Gallego Arias
2020-06-26[declare] Remove Lemmas moduleEmilio Jesus Gallego Arias
2020-06-26[declare] Move proof information to declare.Emilio Jesus Gallego Arias
2020-05-14[exn] [tactics] improve backtraces on monadic errorsEmilio Jesus Gallego Arias
2020-05-10No more local reduction functions in Reductionops.Pierre-Marie Pédrot
2020-05-07[declare] Merge DeclareDef into DeclareEmilio Jesus Gallego Arias
2020-04-28Return an option in lookup_scheme.Pierre-Marie Pédrot
2020-04-21Merge PR #11896: Use lists instead of arrays in evar instances.Maxime Dénès
2020-04-16Merge PR #11861: [declare] [rewrite] Use high-level declare APIPierre-Marie Pédrot
2020-04-15[proof] Merge `Pfedit` into proofs.Emilio Jesus Gallego Arias
2020-04-06Use lists instead of arrays in evar instances.Pierre-Marie Pédrot
2020-03-31[declare] [rewrite] Use high-level declare API, part II.Emilio Jesus Gallego Arias
2020-03-31[declare] [rewrite] Use high-level declare API, part I.Emilio Jesus Gallego Arias
2020-03-19Merge PR #11735: Deprecating catchable_exceptionPierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-13Replacing catchable_exception by noncritical in try-with blocks.Hugo Herbelin
2020-02-12Standardize constr -> globref operations to use destRef/isRef/isRefXGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Rewrite.symmetry_inGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Rewrite.default_morphismGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Rewrite.build_morphism_signatureGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Rewrite.resolve_morphismGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Rewrite.decompose_app_relGaëtan Gilbert
2019-12-16Pretyping.check_evars: make initial evar map optionalGaëtan Gilbert
2019-12-10Side-effect free wrapper around already declared schemes.Pierre-Marie Pédrot
2019-11-26Undeprecate Add Setoid / Add Morphism.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:57:37 +0000