dolmen
forked from gbury/dolmen
Star 1
Fork 0
Watch

Version history of src/interface/term.ml

August 2026

Guillaume Bury
Implement 'dumb' polymophism for SMT-LIB + various HO fixes (#268)
committed

July 2026

Guillaume Bury
Split HO into a separate builtin theory for typechecking (#267)
committed
Guillaume Bury
Add Integer exponentiation (#259)
committed

April 2025

Guillaume Bury
Support for SMT-LIB 2.7 (#235)
committed

March 2025

Basile Clément
feat: Support more Alt-Ergo primitives (#220)
committed

March 2024

Guillaume Bury
Add typing extensions, and the bvconv extension (#208)
committed

June 2023

Pierre Villemot
Proper handling of in_interval and bounds in triggers
committed
Hichem R. A
Support more Bit-Vector primitives in Alt-Ergo's native language (#136)
committed
Guillaume Bury
Add printing of type definitions in debug output (#157)
committed

May 2023

Guillaume Bury
Model fixes (#151)
committed

January 2023

Guillaume Bury
Multliple fixes for recursive definitions (#123)
committed

October 2022

Hichem R. A
Expose Term Consts (#112)
committed

June 2022

Guillaume Bury
Better handling of corner cases in models + adjusted err/warn messages
committed
Guillaume Bury
Fix unused warning on type wildcards
committed
Guillaume Bury
Working first prototype
committed
Guillaume Bury
Add response class for parsing provers responses
committed
Hichem R. A
Complete and fix alt-ergo's native language typing (#89)
committed

November 2021

HRA
Add support for Alt-Ergo's built-ins (#87)
committed

May 2021

Guillaume Bury
Add abstraction for Names and Paths
committed
François Bobot
Fixes to_int (#70)
committed
Guillaume Bury
Fix multi-trigger tag
committed

April 2021

Guillaume Bury
Avoid exponential explosion whe handling let binders
committed
Guillaume Bury
Some more fixes
committed
Guillaume Bury
Fix inference problems for tptp
committed
Guillaume Bury
Fix missing builtin for dimacs
committed
Guillaume Bury
Add higher-order type-checking to Dolmen (#66)
committed
Guillaume Bury
Correctly handle parallel let-bindings (#63)
committed

February 2021

François Bobot
[RFC] Add polymorphism of smt v3 in smt v2.6 (#53)
committed

July 2020

Guillaume Bury
Optimize lookups, using maps instead of spelll indexes
committed
Guillaume Bury
Add String theory
committed
Guillaume Bury
Properly handle ADTs in SMTLIBv2.6
committed

May 2020

Guillaume Bury
Better filters and some fixes for SMTLIB2 typing
committed
Guillaume Bury
Lots of fixes + reworked arith filters
committed
François Bobot
Fixes #28 (#31)
committed

February 2020

Guillaume Bury
Add type annotation type-checking
committed
Guillaume Bury
Typechecking and LSP server
committed

November 2018

Guillaume Bury
Replace ocamlbuild with dune (#13)
committed