diff options
| author | Maxime Dénès | 2017-05-11 13:06:47 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-11 13:06:47 +0200 |
| commit | e302b4dbc88c5776155c770aa90134edb571b738 (patch) | |
| tree | cbb6d8a40f7e1baa30ce4968589b82b90b63b891 /plugins | |
| parent | a1788978360bd276bef721963e7adc47c1a49881 (diff) | |
| parent | e4262a89d7bc3d9b985d9a4a939f34176581abcb (diff) | |
Merge PR#201: Transparent abstract
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 21419d1f92..3e6ccaf84a 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -812,6 +812,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 (* ********************************************************************* *) |