aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/reduction.mli
Commit message (Expand)AuthorAge
* 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
* "Improved" the form of the inferred type of "match" byGravatar herbelin2010-06-03
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Ensures that let-in's in arities of inductive types work well. Maybe notGravatar herbelin2009-08-11
* pushed evar reduction in kernelGravatar barras2009-02-06
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
* Add the ability to give a transparent_state for conversion, toGravatar msozeau2008-04-20
* Changement des named_contextGravatar gregoire2005-12-02
* compatibility with POWERPCGravatar gregoire2004-11-22
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* Nouvelle en-têteGravatar herbelin2004-07-16
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* nouvel algo de conversion plus uniformeGravatar barras2001-11-29
* types vs constrGravatar herbelin2001-11-20
* Suites modifs du noyau. Univ devient purement fonctionnel.Gravatar barras2001-11-12
* GROS COMMIT:Gravatar barras2001-11-05
* Depliage des let-in dans le test de gardeGravatar herbelin2001-07-03
* amelioration des messages d'erreurs vis a vis des evarsGravatar barras2001-05-23
* amelioration de la structure des universGravatar barras2001-03-28
* amelioration de la consommation memoire de la conversion en eta-expansantGravatar barras2001-03-23
* entetesGravatar filliatr2001-03-15
* Mise en place d'un système optionnel de discharge immédiat; prise en compte...Gravatar herbelin2001-02-14
* Déplacement du type stack de Reduction vers Closure et utilisation pour accÃ...Gravatar herbelin2000-12-26
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* deplacement poly_args; iterateurs sur les segmentsGravatar filliatr2000-11-22
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* docGravatar herbelin2000-10-18
* Touche finale à la réduction du let in dans conv et closureGravatar herbelin2000-10-04
* whd_castapp_stack va de Term dans ReductionGravatar herbelin2000-10-01
* Retrait de whd_ise1_metasGravatar herbelin2000-09-26
* On laisse les LetIn dans les types des constructeurs et des éliminationsGravatar herbelin2000-09-15
* Nouvelle version de frterm; ajout des contextes dans l'enviornnement de rédu...Gravatar herbelin2000-09-14
* Vers la paramétrisation des fonctions de Reduction et vers la fusion deGravatar herbelin2000-09-12
* Correction pour make docGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Retrait de decomp_prod non conforme à sa specGravatar herbelin2000-06-02
* Mise en place d'un choix constr/typed_type en remplacement de certains CastGravatar herbelin2000-06-01
* suppression de l'env/sigma dans les fonctions de reduction beta et iota seulsGravatar herbelin2000-05-22
* Restructuration des outils pour les inductifs.Gravatar herbelin2000-05-18
* Ajout d'un strong 'light'Gravatar herbelin2000-05-05
* Renommage try_mutind_of en find_inductive (on fait ce qu'on peut !)Gravatar herbelin2000-05-04
* Plus besoin de env dans reduce_mind_case; make_arity et make_constructor sort...Gravatar herbelin2000-03-21
* Correction bug des réduction 'deltat' et renommage 'deltat' en 'evar'Gravatar herbelin2000-03-17
* Nouveaux types 'constructor' et 'inductive' dans Term;Gravatar herbelin1999-12-15
* debug discharge et inductifsGravatar filliatr1999-12-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-04 23:43:14 +0000