blob: 8d2a125c1d57906dff6cd63a7b903bea9627cbfa (
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.
Hypothesis e depends on the body of H'
|
