aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2020-02-11Merge PR #11235: Add syntax for non maximal implicit argumentsHugo Herbelin
2020-02-07Remove unsafe_type_of from funindGaëtan Gilbert
2020-02-07various unsafe_type_of -> type_of_variable in funindGaëtan Gilbert
2020-02-07Remove confusing commented code in funindGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in CcalgoGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Cctac (with small refactor)Gaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Coq_omega.destructure_hypsGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Extractactics.destauto_inGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Extractactics.mkCaseEqGaë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
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-04Add syntax for non maximally inserted implicit argumentsSimonBoulier
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:29:47 +0000