From 5c82bcd1f87cc893319f2553c81a73c69b13b54d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 13 Aug 2014 18:02:11 +0200
Subject: Reorganisation of intropattern code - emphasizing the different kinds
 of patterns - factorizing code of the non-naming intro-patterns

Still some questions:

- Should -> and <- apply to hypotheses or not (currently they apply to
  hypotheses either when used in assert-style tactics or apply in, or
  when the term to rewrite is a variable, in which case "subst" is
  applied)?
- Should "subst" be used when the -> or <- rewrites an equation x=t
  posed by "assert" (i.e. rewrite everywhere and clearing x and hyp)?
- Should -> and <- be applicable in non assert-style if the lemma has
  quantifications?
---
 plugins/decl_mode/decl_proof_instr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/decl_mode')

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index f780d1bb50..702d554fc5 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -735,7 +735,7 @@ let consider_tac c hyps gls =
     | _ ->
 	let id = pf_get_new_id (Id.of_string "_tmp") gls in
 	tclTHEN
-	  (Proofview.V82.of_tactic (forward true None (Some (Loc.ghost, IntroIdentifier id)) c))
+	  (Proofview.V82.of_tactic (pose_proof (Name id) c))
  	  (consider_match false [] [id] hyps) gls
 
 
-- 
cgit v1.2.3