diff options
author | 2015-12-21 22:19:34 +0100 | |
---|---|---|
committer | 2016-06-18 13:09:16 +0200 | |
commit | f841c27c1cfd38aada72f3c8f90e2ed1ec22db6a (patch) | |
tree | 1595db648f65e4f381034a2385f4faa3b88f60cb /ltac | |
parent | 1744e371d8fa2a612e3906c643fb5558a54a484f (diff) |
Adding an "as" clause to specialize.
Comments
--------
- The tactic specialize conveys a somehow intuitive reasoning concept
and I would support continuing maintaining it even if the design
comes in my opinion with some oddities. (Note that the experience of
MathComp and SSReflect also suggests that specialize is an
interesting concept in itself).
There are two variants to specialize:
- specialize (H args) with H an hypothesis looks natural: we
specialize H with extra arguments and the "as pattern" clause comes
naturally as an extension of it, destructuring the result using the
pattern.
- specialize term with bindings makes the choice of fully applying the
term filling missing expressions with bindings and to then behave as
generalize. Wouldn't we like a more fine-grained approach and the
result to remain in the context?
In this second case, the "as" clause works as if the term were posed
in the context with "pose proof".
Diffstat (limited to 'ltac')
-rw-r--r-- | ltac/coretactics.ml4 | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index 321d50df3..de4d589ee 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -142,7 +142,10 @@ END TACTIC EXTEND specialize [ "specialize" constr_with_bindings(c) ] -> [ - Tacticals.New.tclDELAYEDWITHHOLES false c Tactics.specialize + Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c None) + ] +| [ "specialize" constr_with_bindings(c) "as" intropattern(ipat) ] -> [ + Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c (Some ipat)) ] END |