From 676e93c06a448259783f5934f37e1219265b7726 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 15 Oct 2017 17:50:44 -0400 Subject: Add strip_subst_local --- src/Util/TagList.v | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) (limited to 'src/Util/TagList.v') diff --git a/src/Util/TagList.v b/src/Util/TagList.v index 802b7ad92..701039233 100644 --- a/src/Util/TagList.v +++ b/src/Util/TagList.v @@ -26,10 +26,34 @@ Module Tag. => negb loc) ctx. + Definition get_local (ctx : Context) : Context + := List.filter (fun '{| key := k ; value := v ; local := loc |} + => loc) + ctx. + + Ltac subst_from_list ls := + lazymatch eval hnf in ls with + | {| value := ?id |} :: ?ls + => try subst id; subst_from_list ls + | nil => idtac + end. + + Ltac subst_local ctx := + let loc := (eval cbv [get_local List.filter add add_local add_gen] + in (get_local ctx)) in + subst_from_list loc. + Ltac strip_local ctx := let upd := (eval cbv [strip_local negb List.filter] in strip_local) in eval cbv [add add_local add_gen] in (upd ctx). + Ltac strip_subst_local ctx := + let ret := strip_local ctx in + let dummy := match goal with + | _ => subst_local ctx + end in + ret. + Ltac update ctx key value := constr:(add key value ctx). -- cgit v1.2.3