aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
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
2020-02-06unsafe_type_of -> get_type_of in Firstorded.Instances.mk_open_instanceGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Sequent.extend_with_auto_hintsGaëtan Gilbert
2020-02-03Fix efficiency regression #11436Frédéric Besson
2020-01-30Do not rely on Libobject for the current environment in extraction.Pierre-Marie Pédrot
2020-01-30Merge PR #11307: Remove the hacks relying on hardwired libobject tags.Maxime Dénès
2020-01-28Fix #11467Pierre Roux
2020-01-17Merge PR #11362: Lia bugfix 11191Maxime Dénès
2020-01-14[zify] elim let in MLFrédéric Besson
2020-01-08Factorize ascii extraction in ExtrOcamlChar.vMaxime Dénès
2020-01-08Better extraction of string literals in HaskellMaxime Dénès
2020-01-08Reimplement string <-> char list conversionsXavier Leroy
2020-01-08Typo in commentXavier Leroy
2020-01-08Rename ExtrOcamlStringPlus into ExtrOcamlNativeStringXavier Leroy
2020-01-08Avoid hardcoded paths in extractionMaxime Dénès
2020-01-08Avoid warning 40Maxime Dénès
2020-01-08Support extraction of Coq's string type to OCaml's string type, continuedXavier Leroy
2020-01-08Support extraction of Coq's string type to OCaml's string typeXavier Leroy
2020-01-06[micromega] fix of bug #11191Frédéric Besson
2020-01-03Merge PR #11343: fix: Shorten ssrsetoid.v to fix TC performance issueEnrico Tassi
2019-12-31Merge PR #11338: Remove uses of Global in Evd API.Gaëtan Gilbert
2019-12-27fix: Shorten ssrsetoid.vErik Martin-Dorel
2019-12-26Remove uses of Global in Evd API.Pierre-Marie Pédrot
2019-12-26[omega] Remove non-documented "omega with *"Emilio Jesus Gallego Arias
2019-12-26Deprecate the "omega with *" syntax.Pierre-Marie Pédrot
2019-12-22Rename files with Class in their name to make their role clearer.Pierre-Marie Pédrot
2019-12-22Remove the hacks relying on hardwired libobject tags.Pierre-Marie Pédrot
2019-12-18Merge PR #11027: Cleanup post #10647 (expose comind universe handling)Pierre-Marie Pédrot
2019-12-18Merge PR #11203: Make the string argument of `time` print correctlyPierre-Marie Pédrot
2019-12-17[micromega] fix efficiency regressionFrédéric Besson
2019-12-16Pretyping.check_evars: make initial evar map optionalGaëtan Gilbert
2019-12-13[micromega] Enable ocamlformat.Emilio Jesus Gallego Arias
2019-12-11Remove the reliance of ring objects on the named part.Pierre-Marie Pédrot
2019-12-10Side-effect free wrapper around already declared schemes.Pierre-Marie Pédrot
2019-12-06Make the string argument of `time` print correctlyJason Gross
2019-12-06Moving the diversity of constr printers to a label style.Hugo Herbelin
2019-12-05Merge PR #11241: Unfortunate Coq 8.10 bug with "cofix with" tactic syntaxEmilio Jesus Gallego Arias
2019-12-05Unfortunate bug with "cofix with": case of a CProdN over no bindings.Hugo Herbelin
2019-12-05Merge PR #11210: Tacinterp: push_trace doesn't need to be wrapped in a tacticPierre-Marie Pédrot
2019-11-30Actually deprecate the `cutrewrite` tacticMaxime Dénès
2019-11-29Merge PR #11184: Undeprecate Add Setoid / Add Morphism.Pierre-Marie Pédrot
2019-11-29Merge PR #11076: Remove all remaining calls to “omega” from the standard ...Emilio Jesus Gallego Arias
2019-11-29Merge PR #11186: Remove undocumented and deprecated `Congruence Depth` optionPierre-Marie Pédrot
2019-11-28Tacinterp: push_trace doesn't need to be wrapped in a tacticGaëtan Gilbert
2019-11-26Remove undocumented and deprecated `Congruence Depth` optionMaxime Dénès
2019-11-26Fix #11039: proof of False with template poly and nonlinear universesGaëtan Gilbert
2019-11-26Undeprecate Add Setoid / Add Morphism.Théo Zimmermann
2019-11-25Nsatz: use “lia” rather than “omega”Vincent Laporte
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:16:09 +0000