From e430e9823960a136ee65c5977d89113574413449 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 27 Aug 2017 20:22:12 +0200
Subject: Fix semantics of the solve tactical.

---
 theories/Notations.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Notations.v b/theories/Notations.v
index 2a496b3faf..ea31d4ef47 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -84,7 +84,7 @@ Ltac2 rec solve0 tacs :=
 match tacs with
 | [] => Control.zero Tactic_failure
 | tac :: tacs =>
-  Control.enter (fun _ => orelse (fun _ => complete tac) (fun _ => first0 tacs))
+  Control.enter (fun _ => orelse (fun _ => complete tac) (fun _ => solve0 tacs))
 end.
 
 Ltac2 Notation "solve" "[" tacs(list0(thunk(tactic(6)), "|")) "]" := solve0 tacs.
-- 
cgit v1.2.3