965a989dc2
Some macros expand a command into multiple commands. We should not interrupt the elaboration of the command sequence when one fails.
8 lines
265 B
Text
8 lines
265 B
Text
auxDeclIssue.lean:5:3: error: tactic 'assumption' failed,
|
|
⊢ False
|
|
auxDeclIssue.lean:11:2: error: tactic 'subst' failed, did not find equation for eliminating 'x'
|
|
x y : Nat
|
|
⊢ x=y
|
|
auxDeclIssue.lean:18:3: error: tactic 'assumption' failed,
|
|
ex1 : False
|
|
⊢ False
|