diff options
| -rw-r--r-- | theories/Notations.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |