From f841c27c1cfd38aada72f3c8f90e2ed1ec22db6a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 21 Dec 2015 22:19:34 +0100
Subject: 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".
---
 test-suite/success/specialize.v | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v
index 3faa1ca43a..fba05cd902 100644
--- a/test-suite/success/specialize.v
+++ b/test-suite/success/specialize.v
@@ -64,3 +64,11 @@ assert (H:=H I).
 match goal with H:_ |- _ => clear H end.
 match goal with H:_ |- _ => exact H end.
 Qed.
+
+(* Test specialize as *)
+
+Goal (forall x, x=0) -> 1=0.
+intros.
+specialize (H 1) as ->.
+reflexivity.
+Qed.
-- 
cgit v1.2.3