extraction.mli « extraction « contrib - coq - the Coq proof assistant

about summary refs log tree commit diff homepage

path: root/contrib/extraction/extraction.mli

blob: 71c9c9be27c0b24c566b817557610b00db9ec509 (plain)


(*i $Id$ i*)

open Names
open Miniml

val extract : section_path list -> ml_decl list