From 17eb4ec87e101d83bfac94760b6c96db4cc12da2 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 12 Aug 2020 21:11:04 +0200
Subject: [PATCH] also set Suggest Proof Using

---
 theories/options.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/options.v b/theories/options.v
index 907e59ce4..a228ffdf6 100644
--- a/theories/options.v
+++ b/theories/options.v
@@ -2,4 +2,6 @@
 (* Everything here should be [Export Set], which means when this
 file is *imported*, the option will only apply on the import site
 but not transitively. *)
+
 Export Set Default Proof Using "Type".
+Export Set Suggest Proof Using. (* also warns about forgotten [Proof.] *)
-- 
GitLab