aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/sign.ml
Commit message (Expand)AuthorAge
* Modulification of identifierGravatar ppedrot2012-12-14
* More monomorphizationsGravatar ppedrot2012-11-13
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Noise for nothingGravatar pboutill2012-03-02
* Environ: generic equality on named_context replaced by named_context_equalGravatar puech2011-07-29
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Added a few informations about file lineages (for the most part in kernel)Gravatar herbelin2010-05-09
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
* bug in accessing n-th abstractionGravatar barras2008-01-18
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* Suppression des type_app et body_of_type qui alourdissent inutilement le codeGravatar herbelin2007-08-27
* Ajout iter_rel_context/iter_named_contextGravatar herbelin2006-09-01
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* Changement des named_contextGravatar gregoire2005-12-02
* Added map_named_contextGravatar herbelin2005-02-18
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* Nouvelle en-têteGravatar herbelin2004-07-16
* bug #266 (Search Error si on calcule apres avoir fait Clear d'une var Local)Gravatar barras2003-12-16
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* resolution du pb d'efficacite du a Sign.add_named_declGravatar barras2002-04-04
* code redondantGravatar herbelin2002-03-22
* suppression de pop_namedGravatar barras2002-02-22
* - Reforme de la gestion des args recursifs (via arbres reguliers)Gravatar barras2002-02-14
* compat ocaml 3.03Gravatar filliatr2001-12-13
* Ajout mkArityGravatar herbelin2001-11-20
* types vs constrGravatar herbelin2001-11-20
* Suites modifs du noyau. Univ devient purement fonctionnel.Gravatar barras2001-11-12
* GROS COMMIT:Gravatar barras2001-11-05
* Suppression option immediate_discharge; nettoyage de Declare et conséquencesGravatar herbelin2001-10-11
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* Correction messages d'erreurGravatar herbelin2001-10-03
* exceptionsGravatar barras2001-09-14
* mauvais rattrapage d'exceptionGravatar barras2001-09-14
* entetesGravatar filliatr2001-03-15
* Mise en place d'un système optionnel de discharge immédiat; prise en compte...Gravatar herbelin2001-02-14
* Prise en compte des let in dans les instances de globauxGravatar herbelin2000-11-27
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* Rebranchement de la tactique LetGravatar herbelin2000-10-03
* 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
* Renommage hypothèses de nom redondant dans les environnementsGravatar herbelin2000-05-22
* Abstraction de l'implémentation des signatures de Sign en vue intégration d...Gravatar herbelin2000-01-26
* - Typing -> Safe_typingGravatar filliatr1999-12-01
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 21:27:27 +0000