The tactic remember now accepts a final eqn:H option (grant wish #2489)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15567 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 22 insertions, 16 deletions

diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 20b70cef42..990043ada8 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -63,12 +63,15 @@ let h_generalize cl =
     cl)
 let h_generalize_dep c =
   abstract_tactic (TacGeneralizeDep c) (generalize_dep c)
-let h_let_tac b na c cl =
-  let with_eq = if b then None else Some (true,(Loc.ghost,IntroAnonymous)) in
-  abstract_tactic (TacLetTac (na,c,cl,b)) (letin_tac with_eq na c None cl)
-let h_let_pat_tac b na c cl =
-  let with_eq = if b then None else Some (true,(Loc.ghost,IntroAnonymous)) in
-  abstract_tactic (TacLetTac (na,snd c,cl,b))
+let h_let_tac b na c cl eqpat =
+  let id = Option.default (Loc.ghost,IntroAnonymous) eqpat in
+  let with_eq = if b then None else Some (true,id) in
+  abstract_tactic (TacLetTac (na,c,cl,b,eqpat))
+    (letin_tac with_eq na c None cl)
+let h_let_pat_tac b na c cl eqpat =
+  let id = Option.default (Loc.ghost,IntroAnonymous) eqpat in
+  let with_eq = if b then None else Some (true,id) in
+  abstract_tactic (TacLetTac (na,snd c,cl,b,eqpat))
     (letin_pat_tac with_eq na c None cl)
 
 (* Derived basic tactics *)
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 3028d3a1e2..12791dfb5f 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -57,10 +57,11 @@ val h_cut             : constr -> tactic
 val h_generalize      : constr list -> tactic
 val h_generalize_gen  : (constr Locus.with_occurrences * name) list -> tactic
 val h_generalize_dep  : constr -> tactic
-val h_let_tac         : letin_flag -> name -> constr ->
-                        Locus.clause -> tactic
+val h_let_tac         : letin_flag -> name -> constr -> Locus.clause ->
+                        intro_pattern_expr located option -> tactic
 val h_let_pat_tac     : letin_flag -> name -> evar_map * constr ->
-                        Locus.clause -> tactic
+                        Locus.clause -> intro_pattern_expr located option ->
+                        tactic
 
 (** Derived basic tactics *)
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 3eddb1aaef..d7ac1e66e5 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -718,10 +718,11 @@ let rec intern_atomic lf ist x =
 	               intern_constr_with_occurrences ist c,
                        intern_name lf ist na) cl)
   | TacGeneralizeDep c -> TacGeneralizeDep (intern_constr ist c)
-  | TacLetTac (na,c,cls,b) ->
+  | TacLetTac (na,c,cls,b,eqpat) ->
       let na = intern_name lf ist na in
       TacLetTac (na,intern_constr ist c,
-                 (clause_app (intern_hyp_location ist) cls),b)
+                 (clause_app (intern_hyp_location ist) cls),b,
+		 (Option.map (intern_intro_pattern lf ist) eqpat))
 
   (* Automation tactics *)
   | TacTrivial (d,lems,l) -> TacTrivial (d,List.map (intern_constr ist) lems,l)
@@ -2398,18 +2399,18 @@ and interp_atomic ist gl tac =
       tclTHEN
 	(tclEVARS sigma)
 	(h_generalize_dep c_interp)
-  | TacLetTac (na,c,clp,b) ->
+  | TacLetTac (na,c,clp,b,eqpat) ->
       let clp = interp_clause ist gl clp in
       if clp = Locusops.nowhere then
-        (* We try to fully-typechect the term *)
+        (* We try to fully-typecheck the term *)
 	let (sigma,c_interp) = pf_interp_constr ist gl c in
 	tclTHEN
 	  (tclEVARS sigma)
-          (h_let_tac b (interp_fresh_name ist env na) c_interp clp)
+          (h_let_tac b (interp_fresh_name ist env na) c_interp clp eqpat)
       else
         (* We try to keep the pattern structure as much as possible *)
         h_let_pat_tac b (interp_fresh_name ist env na)
-          (interp_pure_open_constr ist env sigma c) clp
+          (interp_pure_open_constr ist env sigma c) clp eqpat
 
   (* Automation tactics *)
   | TacTrivial (debug,lems,l) ->
@@ -2854,7 +2855,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacGeneralize cl ->
       TacGeneralize (List.map (on_fst (subst_constr_with_occurrences subst))cl)
   | TacGeneralizeDep c -> TacGeneralizeDep (subst_glob_constr subst c)
-  | TacLetTac (id,c,clp,b) -> TacLetTac (id,subst_glob_constr subst c,clp,b)
+  | TacLetTac (id,c,clp,b,eqpat) ->
+    TacLetTac (id,subst_glob_constr subst c,clp,b,eqpat)
 
   (* Automation tactics *)
   | TacTrivial (d,lems,l) -> TacTrivial (d,List.map (subst_glob_constr subst) lems,l)