aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/cbv.mli
Commit message (Expand)AuthorAge
* Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* Cbv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Gravatar Pierre Letouzey2016-07-03
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Modulification of nameGravatar ppedrot2012-12-18
* Updating headers.Gravatar herbelin2012-08-08
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* fixed CBV strategy: it was too eager on terms likeGravatar barras2009-04-21
* pushed evar reduction in kernelGravatar barras2009-02-06
* subst. explicites avec vecteursGravatar barras2006-05-09
* Nouvelle en-têteGravatar herbelin2004-07-16
* nouvel algo de conversion plus uniformeGravatar barras2001-11-29
* GROS COMMIT:Gravatar barras2001-11-05
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* Nettoyage/restructuration des ensembles d'indicateurs de réductionsGravatar herbelin2001-07-02
* entetesGravatar filliatr2001-03-15
* nouvelle implantation de la reductionGravatar barras2001-03-01
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-01 18:55:51 +0000