Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | micromega : more robust generation of proof terms | Frédéric Besson | 2016-09-07 |
| | | | | | | | - 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) | ||
* | Fix Bug #5005 : micromega tactics is now robust to failure of 'abstract'. | Frédéric Besson | 2016-08-31 |
| | | | | If 'abstract' fails e.g. if there are existentials. The tactic runs an abstract-free alternative. | ||
* | Micromega: qualify Coq.micromega.Tauto (avoid coqdep warnings about new ↵ | Pierre Letouzey | 2016-05-19 |
| | | | | Init/Tauto.v) | ||
* | Update copyright headers. | Maxime Dénès | 2016-01-20 |
| | |||
* | Update headers. | Maxime Dénès | 2015-01-12 |
| | |||
* | micromega : vm_compute; reflexivity -> vm_cast_no_check (eq_refl true) | Frédéric Besson | 2014-08-01 |
| | | | | * Thanks to G. Melquiond for pointing out that 'abstract' already performs type-checking | ||
* | micromega : improve efficiency/termination of type-checking | Frédéric Besson | 2014-08-01 |
| | | | | | * unused terms are generalised * proof is abstract | ||
* | micromega: removal of spurious Export; addition of Lia.v encapsulating lia ↵ | Frédéric Besson | 2013-12-20 |
and nia. |