Add strip_subst_local

1 files changed, 24 insertions, 0 deletions

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).