diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-06-10 19:12:49 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-25 15:13:25 -0400 |
| commit | 5f3d20dc53ffd0537a84c93acd761c3c69081342 (patch) | |
| tree | b82efa45c4430b08562b91cf028edef17b97fe34 /plugins | |
| parent | 11aaa1fd8230a347f1dca1a0f349ea7c7f2768c3 (diff) | |
Add transparent_abstract tactic
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/extratactics.ml4 | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 38fdfb759..a96623a5f 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 (* ********************************************************************* *) |