aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/micromega/Lia.v
Commit message (Expand)AuthorAge
* micromega : more robust generation of proof termsGravatar Frédéric Besson2016-09-07
* Fix Bug #5005 : micromega tactics is now robust to failure of 'abstract'.Gravatar Frédéric Besson2016-08-31
* Micromega: qualify Coq.micromega.Tauto (avoid coqdep warnings about new Init/...Gravatar Pierre Letouzey2016-05-19
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* micromega : vm_compute; reflexivity -> vm_cast_no_check (eq_refl true)Gravatar Frédéric Besson2014-08-01
* micromega : improve efficiency/termination of type-checkingGravatar Frédéric Besson2014-08-01
* micromega: removal of spurious Export; addition of Lia.v encapsulating lia an...Gravatar Frédéric Besson2013-12-20