Mentions légales du service

Skip to content

Use define-rec-fun/s for smtv26-par

François Bobot requested to merge fix_smt_par_printer_ambiguous_application into master

Allows provers to see recursive definitions as definitions and not as axioms

And fix ambiguous parametric application.

Merge request reports