aboutsummaryrefslogtreecommitdiff
path: root/plugins/omega
AgeCommit message (Expand)Author
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
2017-06-01Fix bug #5019 (looping zify on dependent types)Jason 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-26Merge PR#666: romega revisited : no more normalization trace, cleaned-up reso...Maxime Dénès
2017-05-24[option] Remove support for non-synchronous options.Emilio Jesus Gallego Arias
2017-05-22refl_omega: some code refactoringPierre Letouzey
2017-05-22ROmega : merge O_CONSTANT* into a single O_BAD_CONSTANTPierre Letouzey
2017-04-27Fix 4.04 warningsGaetan Gilbert
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-03-24Merge branch 'trunk' into pr379Maxime Dénès
2017-02-17Moving the Ltac plugin to a pack-based one.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
2017-02-14Contradiction API using EConstr.Pierre-Marie Pédrot
2017-02-14Tactics API using EConstr.Pierre-Marie Pédrot
2017-02-14Tacmach API using EConstr.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:38:39 +0000