From 5f3d20dc53ffd0537a84c93acd761c3c69081342 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 10 Jun 2016 19:12:49 -0400
Subject: Add transparent_abstract tactic

---
 plugins/ltac/extratactics.ml4 | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'plugins/ltac/extratactics.ml4')

diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 38fdfb7599..a96623a5f6 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -815,6 +815,19 @@ TACTIC EXTEND destauto
 | [ "destauto" "in" hyp(id) ] -> [ destauto_in id ]
 END
 
+(**********************************************************************)
+
+(**********************************************************************)
+(* A version of abstract constructing transparent terms               *)
+(* Introduced by Jason Gross and Benjamin Delaware in June 2016       *)
+(**********************************************************************)
+
+TACTIC EXTEND transparent_abstract
+| [ "transparent_abstract" tactic3(t) ] -> [ Proofview.Goal.nf_enter { enter = fun gl ->
+      Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) } ]
+| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> [ Proofview.Goal.nf_enter { enter = fun gl ->
+      Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) } ]
+END
 
 (* ********************************************************************* *)
 
-- 
cgit v1.2.3


From 02d2f34e5c84f0169e884c07054a6fbfef9f365c Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:04:58 +0200
Subject: Remove some unused values and types

---
 plugins/ltac/extratactics.ml4 | 2 --
 1 file changed, 2 deletions(-)

(limited to 'plugins/ltac/extratactics.ml4')

diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 38fdfb7599..35cfe8b542 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -52,8 +52,6 @@ let replace_in_clause_maybe_by ist c1 c2 cl tac =
 let replace_term ist dir_opt c cl =
   with_delayed_uconstr ist c (fun c -> replace_term dir_opt c cl)
 
-let clause = Pltac.clause_dft_concl
-
 TACTIC EXTEND replace
    ["replace" uconstr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ]
 -> [ replace_in_clause_maybe_by ist c1 c2 cl tac ]
-- 
cgit v1.2.3


From 4e84e83911c1cf7613a35b921b1e68e097f84b5a Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:11:47 +0200
Subject: Remove unused [open] statements

---
 plugins/ltac/extratactics.ml4 | 1 -
 1 file changed, 1 deletion(-)

(limited to 'plugins/ltac/extratactics.ml4')

diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 35cfe8b542..21419d1f92 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -21,7 +21,6 @@ open Tacexpr
 open Glob_ops
 open CErrors
 open Util
-open Evd
 open Termops
 open Equality
 open Misctypes
-- 
cgit v1.2.3


From b82f27726f5ae891689e3b958323c2a61d4c154b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 15 May 2017 22:31:08 +0200
Subject: Fixing grammar for "evar" by exporting the test_lpar_id_colon trick
 to EXTEND.

---
 plugins/ltac/extratactics.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ltac/extratactics.ml4')

diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 3e6ccaf84a..bd48614dbc 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -463,7 +463,7 @@ open Evar_tactics
 (* TODO: add support for some test similar to g_constr.name_colon so that
    expressions like "evar (list A)" do not raise a syntax error *)
 TACTIC EXTEND evar
-  [ "evar" "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name id) typ ]
+  [ "evar" test_lpar_id_colon "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name id) typ ]
 | [ "evar" constr(typ) ] -> [ let_evar Anonymous typ ]
 END
 
-- 
cgit v1.2.3