diff options
| author | Pierre-Marie Pédrot | 2020-04-10 13:12:49 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-10 13:12:49 +0200 |
| commit | f373d82ffa7d30df6ace77f7064d4eed6f321b90 (patch) | |
| tree | 52f34212ef28f20d52ff7558e74391cae7ed8dfb /user-contrib | |
| parent | 4a3f3bb73bce337137a9deba3d67115a8400a74a (diff) | |
| parent | aa889ee516453af65bd74ffedf8ec3761f97eb43 (diff) | |
Merge PR #11882: Adding a short form of Ltac2 Fresh.fresh
Reviewed-by: MSoegtropIMC
Reviewed-by: ppedrot
Ack-by: tchajed
Diffstat (limited to 'user-contrib')
| -rw-r--r-- | user-contrib/Ltac2/Fresh.v | 6 |
1 files changed, 6 insertions, 0 deletions
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. |