From e559dfc4995ae6777d9ff07d34db738cb77a519c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 4 Feb 2020 18:40:24 +0100
Subject: 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".
---
 plugins/ltac/g_tactic.mlg | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'plugins')

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 ->
-- 
cgit v1.2.3