blob: c6786c72ff792d2f362f61471d5aff7dd80376f8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
The command has indeed failed with message:
Ltac call to "extensionality in (var)" failed.
Tactic failure: Not an extensional equality.
The command has indeed failed with message:
Ltac call to "extensionality in (var)" failed.
Tactic failure: Not an extensional equality.
The command has indeed failed with message:
Ltac call to "extensionality in (var)" failed.
Tactic failure: Not an extensional equality.
The command has indeed failed with message:
Ltac call to "extensionality in (var)" failed.
Tactic failure: Not an extensional equality.
The command has indeed failed with message:
Ltac call to "extensionality in (var)" failed.
Tactic failure: Already an intensional equality.
The command has indeed failed with message:
In nested Ltac calls to "extensionality in (var)" and
"clearbody (ne_var_list)", last call failed.
Error: Hypothesis e depends on the body of H'
|
