v1.1.0

What's Changed

• Proving application propagation lemma by @berpeti in #435
• Various improvements for substitution, equality elimination by @berpeti in #437
• Simultaneous equality elimination for multiple equalities by @Engreyight in #440
• Extend mlRewriteBy notation by @Thrithralas in #441
• Exists singleton, upgrade to Coq 8.20 by @berpeti in #438
• Update proofmode.md by @berpeti in #444

New Contributors

• @Thrithralas made their first contribution in #441

Full Changelog: v1.0.16...v1.1.0

v1.0.16

What's Changed

• Generalize ProductSort to work with patterns (not only symbols) as sorts. by @h0nzZik in #376
• remove some dependency version numbers that we do not use by @h0nzZik in #378
• nix: coq-lsp, cleanup, devShells by @h0nzZik in #379
• update nixpkgs by @h0nzZik in #380
• Use Ltac2 for some foundational tactics by @h0nzZik in #381
• More LTac2 tactics; improve mlApplyMeta. by @h0nzZik in #382
• Opml signature + Pattern by @h0nzZik in #388
• OPML model, model isomorphism, spec of relation to AML model. by @h0nzZik in #389
• oamr_no_junk_fmap by @h0nzZik in #390
• Update nixpkgs by @h0nzZik in #391
• OPML example signature by @h0nzZik in #392
• Update FixpointReasoning.v by @berpeti in #393
• Bool syntax and upgrade to Coq 8.18.0 by @berpeti in #394
• Proofmode tactics for 351 and 357 by @aron64 in #385
• Example opml model: list of bools by @h0nzZik in #400
• Generalize mlReflexivity for all reflexive ML connectives by @berpeti in #401
• Kore import using Pyk 1 -- Sorts by @h0nzZik in #402
• Add mlConj with multiple parameters, improve rewrites by @berpeti in #404
• Cleanup by @h0nzZik in #405
• Generate signature from Kore by @h0nzZik in #408
• Various bugfixes by @berpeti in #409
• Support Coq to 8.17 alongside 8.18 by @h0nzZik in #411
• Generic OPML models by @h0nzZik in #413
• Signature morphisms; signature extension; invertors for model combinators by @h0nzZik in #414
• Example OPML signatures and their extension by @h0nzZik in #415
• Bools theory by @adilido99 in #412
• Improve mlSortedSimpl, theory extension theorem by @berpeti in #420
• Import again 5 by @h0nzZik in #416
• Update proofmode.md by @berpeti in #424
• Default models for simple theories by @berpeti in #428
• Product sort theory by @adilido99 in #429
• Nat theory by @adilido99 in #425
• Sum sort theory by @adilido99 in #430
• Remove unnecessary Ensemble imports and axiom usage in some modules by @berpeti in #432
• Unification by @Engreyight in #431

New Contributors

• @aron64 made their first contribution in #385
• @adilido99 made their first contribution in #412
• @Engreyight made their first contribution in #431

Full Changelog: v1.0.15...v1.0.16

v1.0.15

What's Changed

• Exploratory work on stateless translation of LN into Named by @h0nzZik in #341
• Another exploratory work on LN2Named translation by @h0nzZik in #342
• Refactorings around the Deduction theorem; mlClassic by @h0nzZik in #343
• update nixpkgs; coq 8.17 by @h0nzZik in #345
• Slightly generalize DT by @h0nzZik in #344
• Named UI: preliminaries by @h0nzZik in #347
• Transitivity of ML subseteq by @h0nzZik in #348
• Initial work on Contextual implication by @h0nzZik in #349
• Freshness Manager by @h0nzZik in #350
• Use FreshnessManager in the FO proof mode by @h0nzZik in #360
• Fix nonterminating tactics by @berpeti in #371
• Product sorts (and some other things) by @h0nzZik in #372
• Evaluation with better examples by @berpeti in #369
• make the ProofMode tutorial work again by @h0nzZik in #373
• automatically introduce wf premises when entering proof mode by @h0nzZik in #374

Full Changelog: v1.0.14...v1.0.15

v1.0.14

What's Changed

• Extract proof mode files into a folder by @berpeti in #339

Full Changelog: v1.0.13...v1.0.14

v1.0.13

What's Changed

• disable Alectryon by @h0nzZik in #329
• Evaluation of proof mode by @berpeti in #330
• mlDestructImp and mlRevert by @berpeti in #331
• The general deduction theorem from the 2019 paper by @h0nzZik in #332
• mlDeduct "H": a wrapper tactic for Deduction theorem by @h0nzZik in #333
• remove wflexprod.v by @h0nzZik in #334
• Example: mlRewrite under binders by @h0nzZik in #335
• Equality tactics: mlReflexivity, mlSymmetry by @berpeti in #336
• Move and mark Unification.v as ongoing work by @berpeti in #337

Full Changelog: v1.0.12...v1.0.13

v1.0.12

What's Changed

• Universal generalization/isntantiation to implement a version for mlIntroAll and mlRevertAll by @berpeti in #323
• First-order proof mode tactics: mlDestructEx, mlSpecialize, mlExists by @berpeti in #324
• update to latest nixpkgs, including Coq 8.16.1 by @h0nzZik in #326
• Have a separate typeclass for Symbols of signature by @h0nzZik in #327
• Relative completeness of the proof mode, mlDestructBot by @berpeti in #325

Full Changelog: v1.0.11...v1.0.12

v1.0.11

What's Changed

• Optimisation of mlRewrite, ProofInfo by @berpeti in #320
• Nat.v => Nat_Syntax.v + Nat_ProofSystem.v; cleanup by @h0nzZik in #322

Full Changelog: v1.0.10...v1.0.11

v1.0.10

What's Changed

• Deduction Theorem with KT (rebased) by @h0nzZik in #316
• Begin work on FO proof mode by @h0nzZik in #317
• Theory of natural numbers by @Bxil in #319

New Contributors

• @Bxil made their first contribution in #319

Full Changelog: v1.0.9...v1.0.10

v1.0.7

What's Changed

• Refactoring and substitution classes by @berpeti in #295
• mlApplyMetaGeneralized by @h0nzZik in #306
• Alpha-equivalence of named representation; part of collapse function. by @h0nzZik in #308
• New well-formedness solver by @h0nzZik in #310
• Automatically enter proof mode when a tactic is executed by @h0nzZik in #312

Full Changelog: v1.0.6...v1.0.7

v1.0.6

What's Changed

• Substitution notation are no longer imported implicitly by @h0nzZik in #290
• disable auto update stdpp by @h0nzZik in #302
• preserve the old documentation but squashed by @h0nzZik in #280
• Alectryon snippets by @h0nzZik in #303

Full Changelog: v1.0.5...v1.0.6