aboutsummaryrefslogtreecommitdiff
path: root/plugins/omega
AgeCommit message (Expand)Author
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
2018-02-21Merge PR #6604: Extend `zify_N` with knowledge about `N.pred`Maxime Dénès
2018-02-17Change references to CAMLP4 to CAMLP5 to be more accurate since we noJim Fehrle
2018-02-14Extend `zify_N` with knowledge about `N.pred`Joachim Breitner
2018-02-02Reductionops.nf_* now take an environment.Gaëtan Gilbert
2017-11-23Using is_conv rather than eq_constr to find `nat` or `Z` in omega.Hugo Herbelin
2017-10-05Omega now aware of context variables with bodies (in type Z or nat) (fix bug ...Pierre Letouzey
2017-09-28Efficient fresh name generation relying on sets.Pierre-Marie Pédrot
2017-09-12Port is_Set and is_Type to EConstr, as was is_Prop already.Guillaume Melquiond
2017-07-17[API] Remove `open API` in ml files in favor of `-open API` flag.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-14Merge PR#673: Two fixes about zify (bugs #5336 and #5439)Maxime Dénès
2017-06-13Dualize the unsafe flag of refine into typecheck and make it mandatory.Pierre-Marie Pédrot
2017-06-13Explicit the unsafe flag of all calls to Refine.refine.Pierre-Marie Pédrot
2017-06-12Merge PR#718: API cleanup: aliasesMaxime Dénès
2017-06-12zify: force reduction of (Z.max 0 0) and similar (fix #5439)Pierre Letouzey
2017-06-12zify: confusion between Pos2Z.inj_sub and Pos2Z.inj_sub_max (fix #5336)Pierre Letouzey
2017-06-10Remove remaining vo.itarget files (obsolete since PR #499)Pierre Letouzey
2017-06-10Remove (useless) aliases from the API.Matej Košík
2017-06-08Merge branch 'v8.6'Pierre-Marie Pédrot
2017-06-07Put all plugins behind an "API".Matej Kosik
2017-06-06Remove the Sigma (monotonous state) API.Maxime Dénès
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:13:15 +0000