diff options
| author | Hugo Herbelin | 2020-03-22 20:55:43 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-04-03 20:33:27 +0200 |
| commit | 541a99bcbd0fe761934f7291508c3c604d76f940 (patch) | |
| tree | eb1e9a52d7c05221eb0e7a7190389b426381d443 | |
| parent | c5c8ce135606f311834d4c0b9ac3e72be5ee4a36 (diff) | |
Adding fresh-in-context: a short form of Ltac2 Fresh.fresh.
| -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. |