From d28c22a7b173fc78de98c8bf0f986cb163e210a0 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 15 Mar 2018 23:25:53 +0100 Subject: Make direct invocations of `simple apply` obey `Opaque` directive. When called by auto, `simple apply` still does not respect `Opaque` because of compatibility issues. --- CHANGES | 3 +++ 1 file changed, 3 insertions(+) (limited to 'CHANGES') diff --git a/CHANGES b/CHANGES index e8718bbab..787c9ba12 100644 --- a/CHANGES +++ b/CHANGES @@ -25,6 +25,9 @@ Tactics - Deprecated the Implicit Tactic family of commands. +- The `simple apply` tactic now respects the `Opaque` flag when called from + Ltac (`auto` still does not respect it). + Tools - Coq_makefile lets one override or extend the following variables from -- cgit v1.2.3