From 5de065df4799cb43aba9195bcd88a5f0479884ff Mon Sep 17 00:00:00 2001 From: jadep Date: Wed, 24 Aug 2016 17:09:28 -0400 Subject: Moved a tactic to Util/Tactics.v --- src/Util/Tactics.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src/Util/Tactics.v') diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index be777512c..cee2fc2a1 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -61,6 +61,8 @@ Ltac subst_evars := | [ e := ?E |- _ ] => is_evar E; subst e end. +Ltac subst_let := repeat match goal with | x := _ |- _ => subst x end. + (** destruct discriminees of [match]es in the goal *) (* Prioritize breaking apart things in the context, then things which don't need equations, then simple matches (which can be displayed -- cgit v1.2.3