From c41f5d406f627e94363b4549ef268ffa33e7b681 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 25 Aug 2017 15:01:02 +0200
Subject: Respect the default goal selector in toplevel invocations.

---
 tests/example2.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'tests')

diff --git a/tests/example2.v b/tests/example2.v
index 6b26b78022..95485305dc 100644
--- a/tests/example2.v
+++ b/tests/example2.v
@@ -2,6 +2,8 @@ Require Import Ltac2.Ltac2.
 
 Import Ltac2.Notations.
 
+Set Default Goal Selector "all".
+
 Goal exists n, n = 0.
 Proof.
 split with (x := 0).
-- 
cgit v1.2.3