diff options
| author | Hugo Herbelin | 2020-02-04 18:40:24 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-03 14:21:41 +0100 |
| commit | e559dfc4995ae6777d9ff07d34db738cb77a519c (patch) | |
| tree | 599726a4826154d44aef2cd930f7079cba0eb70b /plugins | |
| parent | ed8ac4195c89ee14d03c80e1d9d3f66665573cbf (diff) | |
Adding an alias "pose proof (x:=a)" for "pose proof a as x".
This is to be consistent with "pose (x:=a)" (and an alternative to
"assert (x:=a)").
This was suggested by
"https://github.com/HoTT/HoTT/pull/1208#discussion_r374342962".
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/g_tactic.mlg | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index f0d6258cd1..fe762b4a1f 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -611,6 +611,16 @@ GRAMMAR EXTEND Gram { TacAtom (CAst.make ~loc @@ TacAssert (false,true,Some tac,ipat,c)) } | IDENT "eassert"; c = constr; ipat = as_ipat; tac = by_tactic -> { TacAtom (CAst.make ~loc @@ TacAssert (true,true,Some tac,ipat,c)) } + + (* Alternative syntax for "pose proof c as id by tac" *) + | IDENT "pose"; IDENT "proof"; test_lpar_id_coloneq; "("; lid = identref; ":="; + c = lconstr; ")" -> + { let { CAst.loc = loc; v = id } = lid in + TacAtom (CAst.make ?loc @@ TacAssert (false,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) } + | IDENT "epose"; IDENT "proof"; test_lpar_id_coloneq; "("; lid = identref; ":="; + c = lconstr; ")" -> + { let { CAst.loc = loc; v = id } = lid in + TacAtom (CAst.make ?loc @@ TacAssert (true,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) } | IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat -> { TacAtom (CAst.make ~loc @@ TacAssert (false,true,None,ipat,c)) } | IDENT "epose"; IDENT "proof"; c = lconstr; ipat = as_ipat -> |