From 1ef1286c43d4d099b3b017069ed09c261eb8b6ca Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Fri, 10 Apr 2020 23:10:34 +0200
Subject: docs: Update CHANGES after issue #479 and PR #480

* Make (coq-insert-intros) conditionnaly insert `move=>` or `intros`
---
 CHANGES | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index cbe2e76d..013dc3be 100644
--- a/CHANGES
+++ b/CHANGES
@@ -135,6 +135,11 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac
     between successive proof steps.  See section 11.8 ("Showing
     Proof Diffs") in the documentation.
 
+*** Support Ssreflect's proof style for inserting an intros tactic
+    when doing "C-c C-a TAB": PG inserts "move=> ..." if the current
+    file contains "Require ... ssreflect" on the same line; otherwise
+    PG inserts "intros ..." as before.
+
 *** bug fixes
     - avoid leaving partial files behind when compilation fails
     - 123: Parallel background compliation fails to execute some
-- 
cgit v1.2.3