diff options
Diffstat (limited to 'theories/Program')
| -rw-r--r-- | theories/Program/Tactics.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index c3870e6bda..ad03de2f40 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -175,4 +175,6 @@ Ltac program_simplify := simpl ; intros ; destruct_conjs ; simpl proj1_sig in * ; subst* ; try autoinjection ; try discriminates ; try (solve [ red ; intros ; destruct_conjs ; try autoinjection ; discriminates ]). -Ltac program_simpl := program_simplify ; auto with *. +Ltac default_program_simpl := program_simplify ; auto with *. + +Ltac program_simpl := default_program_simpl. |