From f8970ec2140662274bb10f0eb8d3ca72924835c7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 31 Dec 2013 16:25:25 +0100 Subject: Proof_using: new syntax + suggestion Proof using can be followed by: - All : all variables - Type : all variables occurring in the type - expr: - (a b .. c) : set - expr + expr : set union - expr - expr : set difference - -expr : set complement (All - expr) Exceptions: - a singleton set can be written without parentheses. This also allows the implementation of named sets sharing the same name space of section hyps ans write - bla - x : where bla is defined as (a b .. x y) elsewhere. - if expr is just a set, then parentheses can be omitted This module also implements some AI to tell the user how he could decorate "Proof" with a "using BLA" clause. Finally, one can Set Default Proof Using "str" to any string that is used whenever the "using ..." part is missing. The coding of this sucks a little since it is the parser that applies the default. --- intf/vernacexpr.mli | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) (limited to 'intf') diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 4f666a801..ee51a7694 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -214,6 +214,14 @@ type scheme = | CaseScheme of bool * reference or_by_notation * sort_expr | EqualityScheme of reference or_by_notation +type section_subset_expr = + | SsSet of lident list + | 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 + (* This type allows to register inline of constants in native compiler. It will be extended with primitive inductive types and operators *) type register_kind = @@ -412,7 +420,7 @@ type vernac_expr = | VernacEndSubproof | VernacShow of showable | VernacCheckGuard - | VernacProof of raw_tactic_expr option * lident list option + | VernacProof of raw_tactic_expr option * section_subset_descr option | VernacProofMode of string (* Toplevel control *) | VernacToplevelControl of exn -- cgit v1.2.3