| 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.
|
|
|
|
| |
Init/Tauto.v)
|
| |
|
| |
|
|
|
|
| |
* Thanks to G. Melquiond for pointing out that 'abstract' already performs type-checking
|
|
|
|
|
| |
* unused terms are generalised
* proof is abstract
|
|
and nia.
|