ExtractToCoq.ml « compiler - aeneas - aeneas rust verifier with a hacky Isabelle backend

summary refs log tree commit diff

path: root/compiler/ExtractToCoq.ml

blob: 3681adc346ccab49b2907165a21eff2c1fc4100e (plain)

(** Utilities for the extraction to Coq *)

open Utils
open Pure
open TranslateCore
open ExtractBase
open StringUtils
module F = Format