blob: 2f7b247ac32bf8da0ae019198e15af9c4b87ec49 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(*i $Id$ i*)
(* This module implements the discharge mechanism. It provides a function to
close the last opened section. That function calls [Lib.close_section] and
then re-introduce all the discharged versions of the objects that were
defined in the section. *)
val close_section : bool -> string -> unit
val save_module_to : string -> string -> unit
|
