From 15b6c9b6fa268a9af6dd4f05961e469545e92a6f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 24 Feb 2014 20:46:32 +0100 Subject: Lazyconstr -> Opaqueproof Make this module deal only with opaque proofs. Make discharging/substitution invariant more explicit via a third constructor. --- library/lib.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'library/lib.mli') diff --git a/library/lib.mli b/library/lib.mli index 787dc969e..8975acd9a 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -187,7 +187,7 @@ val discharge_global : Globnames.global_reference -> Globnames.global_reference val discharge_inductive : Names.inductive -> Names.inductive (* discharging a constant in one go *) -val full_replacement_context : unit -> Lazyconstr.work_list list +val full_replacement_context : unit -> Opaqueproof.work_list list val full_section_segment_of_constant : Names.constant -> (Context.named_context -> Context.named_context) list -- cgit v1.2.3