aboutsummaryrefslogtreecommitdiff
path: root/plugins/omega/coq_omega.ml
AgeCommit message (Expand)Author
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-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
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-10[coqlib] Rebindable Coqlib namespace.Emilio Jesus Gallego Arias
2018-09-24[engine] Remove and deprecate `nf_enter` et al.Emilio Jesus Gallego Arias
2018-07-03Coq_omega: remove unused Goal.entersGaëtan Gilbert
2018-07-03Remove unused function Coq_omega.timing.Gaëtan Gilbert
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-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-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-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
2017-05-29Omega: use "simpl" only on coefficents, not on atoms (fix #4132)Pierre Letouzey
2017-05-29Cleanup: removal of constr_of_global.Matthieu Sozeau
2017-05-29Merge PR#512: [cleanup] Unify all calls to the error function.Maxime Dénès
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
2017-05-27[coqlib] Move `Coqlib` to `library/`.Emilio Jesus Gallego Arias
2017-05-24[option] Remove support for non-synchronous options.Emilio Jesus Gallego Arias
2017-04-24Porting omega to the new tactic API.Pierre-Marie Pédrot
2017-04-24Removing trivial compatibility layer in omega.Pierre-Marie Pédrot
2017-04-07Fix an unhandled exception in Omega.Pierre-Marie Pédrot
2017-04-01Actually exporting delayed universes in the EConstr implementation.Pierre-Marie Pédrot
2017-02-14Removing most nf_enter in tactics.Pierre-Marie Pédrot
2017-02-14Fix a mishandled exception in Omega.Pierre-Marie Pédrot
2017-02-14Definining EConstr-based contexts.Pierre-Marie Pédrot
2017-02-14Omega API using EConstr.Pierre-Marie Pédrot
2017-02-14Removing various compatibility layers of tactics.Pierre-Marie Pédrot
2017-02-14Reductionops now return EConstrs.Pierre-Marie Pédrot
2017-02-14Proofview.Goal primitive now return EConstrs.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 02:55:35 +0000