| Commit message (Collapse) | Author | Age |
| |
|
| |
|
|
|
|
|
|
|
| |
- Assert a purely arihtmetic sub-goal that is proved independently by reflexion.
(This reduces the stress on the conversion test)
- Does not use 'abstract' anymore (more natural proof-term)
- Fix a parsing bug (certain terms in Prop where not recognized)
|
|
|
|
| |
If 'abstract' fails e.g. if there are existentials. The tactic runs an abstract-free alternative.
|
|
(Fixed #4985)
Lqa.v defines the tactics lra and nra working over Q.
Lra.v defines the tactics lra and nra working over R.
|