aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/rewrite.ml
AgeCommit message (Expand)Author
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
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-13Return of Refine Instance as an attribute.Gaëtan Gilbert
2019-08-17Delay the computation of frozen evars in legacy unification.Pierre-Marie Pédrot
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-07-01[decls] Remove goal_object_kind type.Emilio Jesus Gallego Arias
2019-07-01[declare] Separate kinds from entries in constant declarationEmilio Jesus Gallego Arias
2019-07-01[api] Refactor most of `Decl_kinds`Emilio Jesus Gallego Arias
2019-06-26[declare] Fine tuning of Hook type.Emilio Jesus Gallego Arias
2019-06-25Remove the internal_flag argument from Declare API.Pierre-Marie Pédrot
2019-06-24[api] Remove `polymorphic` type alias, use labels instead.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-24[lemmas] Turn Lemmas.info into a proper type with constructor.Emilio Jesus Gallego Arias
2019-06-24Duplicate the type of constant entries in Proof_global.Pierre-Marie Pédrot
2019-06-20Merge PR #9645: [proof] Remove terminator type, unifying regular and obligati...Pierre-Marie Pédrot
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-17[proof] Move declaration hooks to DeclareDef.Emilio Jesus Gallego Arias
2019-06-09[proof] Move proofs that have an associated constant to `Lemmas`Emilio Jesus Gallego Arias
2019-06-08Cleaning the status of Local Definition and similar.Hugo Herbelin
2019-06-07Merge PR #10205: Make discriminate tactic compatible with HoTTPierre-Marie Pédrot
2019-06-06Make discriminate tactic compatible with HoTTAndreas Lynge
2019-06-04[rewrite] remove program_mode from attributes (unused)Enrico Tassi
2019-06-04[classes] remove program mode from the new_instance_* APIsEnrico Tassi
2019-06-04[vernac] more precise types for Add Morph, Instance, and FunctionEnrico Tassi
2019-06-04[rewrite] Add Morphism syntax made different for module type parametersEnrico Tassi
2019-06-04Rename Proof_global.{pstate -> t}Gaëtan Gilbert
2019-06-04coqpp: add new ![] specifiers for structured proof interactionGaëtan Gilbert
2019-06-04Proof_global: pass only 1 pstate when we don't want the proof stackGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 19:51:45 +0000