extraction.mli « extraction « contrib - coq - The formal proof system

about summary refs log tree commit diff

path: root/contrib/extraction/extraction.mli

blob: 71c9c9be27c0b24c566b817557610b00db9ec509 (plain)

(*i $Id$ i*)

open Names
open Miniml

val extract : section_path list -> ml_decl list