From 9ea8867a0fa8f2a52df102732fdc1a931c659826 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 30 Sep 2015 22:12:25 +0200 Subject: Proof using: let-in policy, optional auto-clear, forward closure* - "Proof using p*" means: use p and any section var about p. - Simplify the grammar/parser for proof using . - Section variables with a body (let-in) are pulled in automatically since they are safe to be used (add no extra quantification) - automatic clear of "unused" section variables made optional: Set Proof Using Clear Unused. since clearing section hypotheses does not "always work" (e.g. hint databases are not really cleaned) - term_typing: trigger a "suggest proof using" message also for Let theorems. --- intf/vernacexpr.mli | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'intf') diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 9248fa953c..fd6e1c6ae1 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -225,12 +225,12 @@ type scheme = | EqualityScheme of reference or_by_notation type section_subset_expr = - | SsSet of lident list + | SsEmpty + | SsSingl of lident | SsCompl of section_subset_expr | SsUnion of section_subset_expr * section_subset_expr | SsSubstr of section_subset_expr * section_subset_expr - -type section_subset_descr = SsAll | SsType | SsExpr of section_subset_expr + | SsFwdClose of section_subset_expr (** Extension identifiers for the VERNAC EXTEND mechanism. *) type extend_name = @@ -336,7 +336,7 @@ type vernac_expr = class_rawexpr * class_rawexpr | VernacIdentityCoercion of obsolete_locality * lident * class_rawexpr * class_rawexpr - | VernacNameSectionHypSet of lident * section_subset_descr + | VernacNameSectionHypSet of lident * section_subset_expr (* Type classes *) | VernacInstance of @@ -441,7 +441,7 @@ type vernac_expr = | VernacEndSubproof | VernacShow of showable | VernacCheckGuard - | VernacProof of raw_tactic_expr option * section_subset_descr option + | VernacProof of raw_tactic_expr option * section_subset_expr option | VernacProofMode of string (* Toplevel control *) | VernacToplevelControl of exn -- cgit v1.2.3