diff options
| author | Pierre-Marie Pédrot | 2017-08-27 20:22:12 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-27 20:22:12 +0200 |
| commit | e430e9823960a136ee65c5977d89113574413449 (patch) | |
| tree | e71544176aa458f2d95005a68aa677aa344460ed | |
| parent | 4c822dbb1c01139e95c165515777703263806ec1 (diff) | |
Fix semantics of the solve tactical.
| -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. |