diff options
| author | Hugo Herbelin | 2014-08-02 09:30:30 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-08-05 19:52:21 +0200 |
| commit | 0e6facc70506d81e765c5a0be241a77bc7b22b85 (patch) | |
| tree | ba0f92d3bf019d5cbf4c72b2f2b667457052f179 /parsing | |
| parent | f9517286637fd0891a3ac1aac041b437e157f756 (diff) | |
Adding a syntax "enough" for the variant of "assert" with the order of
subgoals and the role of the "by tac" clause swapped.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 20 |
1 files changed, 14 insertions, 6 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 4c328a3bf2..c02f2d569a 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -569,19 +569,27 @@ GEXTEND Gram p = clause_dft_all -> TacLetTac (na,c,p,false,e) - (* Begin compatibility *) + (* Alternative syntax for "pose proof c as id" *) | IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":="; c = lconstr; ")" -> - TacAssert (None,Some (!@loc,IntroIdentifier id),c) + TacAssert (true,None,Some (!@loc,IntroIdentifier id),c) + + (* Alternative syntax for "assert c as id by tac" *) | IDENT "assert"; test_lpar_id_colon; "("; (loc,id) = identref; ":"; c = lconstr; ")"; tac=by_tactic -> - TacAssert (Some tac,Some (!@loc,IntroIdentifier id),c) - (* End compatibility *) + TacAssert (true,Some tac,Some (!@loc,IntroIdentifier id),c) + + (* Alternative syntax for "enough c as id by tac" *) + | IDENT "enough"; test_lpar_id_colon; "("; (loc,id) = identref; ":"; + c = lconstr; ")"; tac=by_tactic -> + TacAssert (false,Some tac,Some (!@loc,IntroIdentifier id),c) | IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic -> - TacAssert (Some tac,ipat,c) + TacAssert (true,Some tac,ipat,c) | IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat -> - TacAssert (None,ipat,c) + TacAssert (true,None,ipat,c) + | IDENT "enough"; c = constr; ipat = as_ipat; tac = by_tactic -> + TacAssert (false,Some tac,ipat,c) | IDENT "generalize"; c = constr -> TacGeneralize [((AllOccurrences,c),Names.Anonymous)] |