Fixing "pose proof (H ...) as H" and "assert (H:=H ...) which were supposed

to behave like "specialize (H ...)" since 4/8/2008 (r11300, 7d515acbc5).

3 files changed, 11 insertions, 9 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index ea74dc37e..d012427a0 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -540,7 +540,7 @@ let replace_core clause l2r eq =
   if check_setoid clause
   then init_setoid ();
   tclTHENFIRST
-    (assert_as false None eq)
+    (assert_as false None None eq)
     (onLastHypId (fun id ->
       tclTHEN
         (tclTRY (general_rewrite_clause l2r false (mkVar id,NoBindings) clause))
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6d81a4870..661a786b0 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2230,11 +2230,11 @@ let ipat_of_name = function
    let c = fst (decompose_app ((strip_lam_assum c))) in
    if isVar c then Some (destVar c) else None
 
-let assert_as first ipat c =
+let assert_as first hd ipat t =
   let naming,tac = prepare_intros IntroAnonymous ipat in
-  let repl = do_replace (head_ident c) naming in
-  if first then assert_before_then_gen repl naming c tac
-  else assert_after_then_gen repl naming c tac
+  let repl = do_replace hd naming in
+  if first then assert_before_then_gen repl naming t tac
+  else assert_after_then_gen repl naming t tac
 
 (* apply in as *)
 
@@ -2394,16 +2394,17 @@ let forward b usetac ipat c =
   match usetac with
   | None ->
       Proofview.Goal.enter begin fun gl ->
-      let t = Tacmach.New.pf_unsafe_type_of gl  c in
-      Tacticals.New.tclTHENFIRST (assert_as true ipat t)
+      let t = Tacmach.New.pf_unsafe_type_of gl c in
+      let hd = head_ident c in
+      Tacticals.New.tclTHENFIRST (assert_as true hd ipat t)
 	(Proofview.V82.tactic (exact_no_check c))
       end
   | Some tac ->
       if b then
-        Tacticals.New.tclTHENFIRST (assert_as b ipat c) tac
+        Tacticals.New.tclTHENFIRST (assert_as b None ipat c) tac
       else
         Tacticals.New.tclTHENS3PARTS
-          (assert_as b ipat c) [||] tac [|Tacticals.New.tclIDTAC|]
+          (assert_as b None ipat c) [||] tac [|Tacticals.New.tclIDTAC|]
 
 let pose_proof na c = forward true None (ipat_of_name na) c
 let assert_by na t tac = forward true (Some tac) (ipat_of_name na) t
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 0069d100b..ade89fc98 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -348,6 +348,7 @@ val assert_before : Name.t -> types -> unit Proofview.tactic
 val assert_after  : Name.t -> types -> unit Proofview.tactic
 
 val assert_as     : (* true = before *) bool ->
+  (* optionally tell if a specialization of some hyp: *) identifier option ->
   intro_pattern option -> constr -> unit Proofview.tactic
 
 (** Implements the tactics assert, enough and pose proof; note that "by"