Merge PR #11882: Adding a short form of Ltac2 Fresh.fresh

Reviewed-by: MSoegtropIMC
Reviewed-by: ppedrot
Ack-by: tchajed

8 files changed, 22 insertions, 10 deletions

diff --git a/doc/changelog/05-tactic-language/11882-master+ltac2-fresh-in-context.rst b/doc/changelog/05-tactic-language/11882-master+ltac2-fresh-in-context.rst
new file mode 100644
index 0000000000..47e7be4d0e
--- /dev/null
+++ b/doc/changelog/05-tactic-language/11882-master+ltac2-fresh-in-context.rst
@@ -0,0 +1,6 @@
+- **Added:**
+  New Ltac2 function ``Fresh.Free.of_goal`` to return the list of
+  names of declarations of the current goal; new Ltac2 function
+  ``Fresh.in_goal`` to return a variable fresh in the current goal
+  (`#11882 <https://github.com/coq/coq/pull/11882>`_,
+  by Hugo Herbelin).
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index 82055c4752..f78c0ecc1e 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -550,14 +550,14 @@ Ltac intuition_in := repeat (intuition; inv In; inv MapsTo).
    Let's do its job by hand: *)
 
 Ltac join_tac :=
- intros l; induction l as [| ll _ lx ld lr Hlr lh];
-   [ | intros x d r; induction r as [| rl Hrl rx rd rr _ rh]; unfold join;
-     [ | destruct (gt_le_dec lh (rh+2)) as [GT|LE];
+ intros ?l; induction l as [| ?ll _ ?lx ?ld ?lr ?Hlr ?lh];
+   [ | intros ?x ?d ?r; induction r as [| ?rl ?Hrl ?rx ?rd ?rr _ ?rh]; unfold join;
+     [ | destruct (gt_le_dec lh (rh+2)) as [?GT|?LE];
        [ match goal with |- context [ bal ?u ?v ?w ?z ] =>
            replace (bal u v w z)
            with (bal ll lx ld (join lr x d (Node rl rx rd rr rh))); [ | auto]
          end
-       | destruct (gt_le_dec rh (lh+2)) as [GT'|LE'];
+       | destruct (gt_le_dec rh (lh+2)) as [?GT'|?LE'];
          [ match goal with |- context [ bal ?u ?v ?w ?z ] =>
              replace (bal u v w z)
              with (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr); [ | auto]
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 387ab75362..4179765dca 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -1753,7 +1753,7 @@ Qed.
 
 Ltac destr_pggcdn IHn :=
  match goal with |- context [ ggcdn _ ?x ?y ] =>
-  generalize (IHn x y); destruct ggcdn as (g,(u,v)); simpl
+  generalize (IHn x y); destruct ggcdn as (?g,(?u,?v)); simpl
  end.
 
 Lemma ggcdn_correct_divisors : forall n a b,
diff --git a/theories/micromega/Lia.v b/theories/micromega/Lia.v
index f3b70f61d2..3d955fec4f 100644
--- a/theories/micromega/Lia.v
+++ b/theories/micromega/Lia.v
@@ -21,7 +21,7 @@ Declare ML Module "micromega_plugin".
 
 
 Ltac zchecker :=
-  intros __wit __varmap __ff ;
+  intros ?__wit ?__varmap ?__ff ;
   exact (ZTautoChecker_sound __ff __wit
                                 (@eq_refl bool true <: @eq bool (ZTautoChecker __ff __wit) true)
                                 (@find Z Z0 __varmap)).
diff --git a/theories/micromega/Lqa.v b/theories/micromega/Lqa.v
index 786c9275f0..8a4d59b1bd 100644
--- a/theories/micromega/Lqa.v
+++ b/theories/micromega/Lqa.v
@@ -23,7 +23,7 @@ Require Coq.micromega.Tauto.
 Declare ML Module "micromega_plugin".
 
 Ltac rchange := 
-  intros __wit __varmap __ff ;
+  intros ?__wit ?__varmap ?__ff ;
   change (Tauto.eval_bf (Qeval_formula (@find Q 0%Q __varmap)) __ff) ;
   apply (QTautoChecker_sound __ff __wit).
 
diff --git a/theories/micromega/Lra.v b/theories/micromega/Lra.v
index 3ac4772ba4..22cef50e0d 100644
--- a/theories/micromega/Lra.v
+++ b/theories/micromega/Lra.v
@@ -23,7 +23,7 @@ Require Coq.micromega.Tauto.
 Declare ML Module "micromega_plugin".
 
 Ltac rchange := 
-  intros __wit __varmap __ff ;
+  intros ?__wit ?__varmap ?__ff ;
   change (Tauto.eval_bf (Reval_formula (@find R 0%R __varmap)) __ff) ;
   apply (RTautoChecker_sound __ff __wit).
 
diff --git a/theories/setoid_ring/Field_tac.v b/theories/setoid_ring/Field_tac.v
index 89a5ca6740..15b2618e47 100644
--- a/theories/setoid_ring/Field_tac.v
+++ b/theories/setoid_ring/Field_tac.v
@@ -215,7 +215,7 @@ Ltac fold_field_cond req :=
 Ltac simpl_PCond FLD :=
   let req := get_FldEq FLD in
   let lemma := get_CondLemma FLD in
-  try (apply lemma; intros lock lock_def; vm_compute; rewrite lock_def; clear lock_def lock); 
+  try (apply lemma; intros ?lock ?lock_def; vm_compute; rewrite lock_def; clear lock_def lock);
   protect_fv "field_cond";
   fold_field_cond req;
   try exact I.
@@ -223,7 +223,7 @@ Ltac simpl_PCond FLD :=
 Ltac simpl_PCond_BEURK FLD :=
   let req := get_FldEq FLD in
   let lemma := get_CondLemma FLD in
-  (apply lemma; intros lock lock_def; vm_compute; rewrite lock_def; clear lock_def lock);
+  (apply lemma; intros ?lock ?lock_def; vm_compute; rewrite lock_def; clear lock_def lock);
   protect_fv "field_cond";
   fold_field_cond req.
 
diff --git a/user-contrib/Ltac2/Fresh.v b/user-contrib/Ltac2/Fresh.v
index 548bf74a30..5ad9badc8c 100644
--- a/user-contrib/Ltac2/Fresh.v
+++ b/user-contrib/Ltac2/Fresh.v
@@ -9,6 +9,8 @@
 (************************************************************************)
 
 Require Import Ltac2.Init.
+Require Ltac2.Control.
+Require Ltac2.List.
 
 Module Free.
 
@@ -21,8 +23,12 @@ Ltac2 @ external of_ids : ident list -> t := "ltac2" "fresh_free_of_ids".
 
 Ltac2 @ external of_constr : constr -> t := "ltac2" "fresh_free_of_constr".
 
+Ltac2 of_goal () := of_ids (List.map (fun (id, _, _) => id) (Control.hyps ())).
+
 End Free.
 
 Ltac2 @ external fresh : Free.t -> ident -> ident := "ltac2" "fresh_fresh".
 (** Generate a fresh identifier with the given base name which is not a
     member of the provided set of free variables. *)
+
+Ltac2 in_goal id := Fresh.fresh (Free.of_goal ()) id.