aboutsummaryrefslogtreecommitdiff
path: root/plugins/omega
AgeCommit message (Expand)Author
2021-03-03[build] Split stdlib to it's own opam package.Emilio Jesus Gallego Arias
2020-12-21Move evaluable_global_reference from Names to Tacred.Pierre-Marie Pédrot
2020-08-27[numeral] [plugins] Switch from `Big_int` to ZArith.Emilio Jesus Gallego Arias
2020-08-25omega: stop using intro_usingGaëtan Gilbert
2020-05-14[exn] [tactics] improve backtraces on monadic errorsEmilio Jesus Gallego Arias
2020-04-17Deprecate “omega”Vincent Laporte
2020-04-11[dune] [stdlib] Build the standard library natively with Dune.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-13[build] Consolidate stdlib's .v files under a single directory.Emilio Jesus Gallego Arias
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Coq_omega.destructure_hypsGaëtan Gilbert
2020-01-14[zify] elim let in MLFrédéric Besson
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-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-09-16Re-implementation of zifyFrédéric Besson
2019-07-11Merge PR #10498: [api] Deprecate GlobRef constructors.Gaëtan Gilbert
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-07-08[core] [api] Support OCaml 4.08Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-22Partly revert micromega parsing using typeclasses.Frédéric Besson
2019-05-10Split the hypothesis conversion check in a conversion + ordering check.Pierre-Marie Pédrot
2019-04-23Deprecate the *_no_check variants of conversion tactics.Pierre-Marie Pédrot
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-01-24Rename Z.div_mod_to_quot_rem, add Z.quot_rem_to_equations, Z.to_euclidean_div...Jason Gross
2019-01-24Move cleanup from the test-suite to Z.div_mod_to_quot_rem_cleanupJason Gross
2019-01-24Don't bundle Z.div_mod_quot_rem into zifyJason Gross
2019-01-24Don't pose any disjunctions in div_mod_to_quot_remJason Gross
2019-01-24Add Z.div_mod_to_quot_rem tactic, put it in zifyJason Gross
2018-11-23s/let _ =/let () =/ in some places (mostly goptions related)Gaëtan Gilbert
2018-10-18[universes] deprecate constr_of_globalMatthieu Sozeau
2018-10-16[Omega] Remove dead codeVincent Laporte
2018-10-16[omega] Remove dead codeVincent Laporte
2018-10-15Correct some spelling errorsBenjamin Barenblat
2018-10-10[coqlib] Rebindable Coqlib namespace.Emilio Jesus Gallego Arias
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-09-24[engine] Remove and deprecate `nf_enter` et al.Emilio Jesus Gallego Arias
2018-09-18Zify: replace local definitions by equationsVincent Laporte
2018-09-05[build] Preliminary support for building Coq with `dune`.Emilio Jesus Gallego Arias
2018-07-05Merge PR #7746: Many small cleanups removing unused arguments and functionsPierre-Marie Pédrot
2018-07-03Coq_omega: remove unused Goal.entersGaëtan Gilbert
2018-07-03Remove unused function Coq_omega.timing.Gaëtan Gilbert
2018-07-02Moving various ml4 files to mlg.Pierre-Marie Pédrot
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
2018-05-30[api] Remove deprecated object from `Term`Emilio Jesus Gallego Arias
2018-05-25Remove some occurrences of Evd.emptyMaxime Dénès
2018-05-17Split off Universes functions dealing with generating new universes.Gaëtan Gilbert
2018-02-27Update headers following #6543.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:28:40 +0000