aboutsummaryrefslogtreecommitdiff
path: root/kernel/sign.ml
AgeCommit message (Expand)Author
2008-12-31Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->herbelin
2008-01-18bug in accessing n-th abstractionbarras
2007-12-05Factorisation des opérations sur le type option de Util dans un module aspiwack
2007-08-27Suppression des type_app et body_of_type qui alourdissent inutilement le codeherbelin
2006-09-01Ajout iter_rel_context/iter_named_contextherbelin
2006-05-23Nouvelle implantation du polymorphisme de sorte pour les familles inductivesherbelin
2006-04-27Standardisation nom option_app en option_mapherbelin
2005-12-02Changement des named_contextgregoire
2005-02-18Added map_named_contextherbelin
2004-10-20COMMITED BYTECODE COMPILERbarras
2004-07-16Nouvelle en-têteherbelin
2003-12-16bug #266 (Search Error si on calcule apres avoir fait Clear d'une var Local)barras
2002-08-02Modules dans COQ\!\!\!\!coq
2002-04-04resolution du pb d'efficacite du a Sign.add_named_declbarras
2002-03-22code redondantherbelin
2002-02-22suppression de pop_namedbarras
2002-02-14- Reforme de la gestion des args recursifs (via arbres reguliers)barras
2001-12-13compat ocaml 3.03filliatr
2001-11-20Ajout mkArityherbelin
2001-11-20types vs constrherbelin
2001-11-12Suites modifs du noyau. Univ devient purement fonctionnel.barras
2001-11-05GROS COMMIT:barras
2001-10-11Suppression option immediate_discharge; nettoyage de Declare et conséquencesherbelin
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
2001-10-03Correction messages d'erreurherbelin
2001-09-14exceptionsbarras
2001-09-14mauvais rattrapage d'exceptionbarras
2001-03-15entetesfilliatr
2001-02-14Mise en place d'un système optionnel de discharge immédiat; prise en compte...herbelin
2000-11-27Prise en compte des let in dans les instances de globauxherbelin
2000-11-02suppression des (* open Generic *)filliatr
2000-10-18Simplifications autour de typed_type (renommé types par analogie avec sorts)...herbelin
2000-10-18Renommage canonique :herbelin
2000-10-03Rebranchement de la tactique Letherbelin
2000-09-10Correction pour make docherbelin
2000-09-10Ajout d'un LetIn primitif.herbelin
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
2000-05-22Renommage hypothèses de nom redondant dans les environnementsherbelin
2000-01-26Abstraction de l'implémentation des signatures de Sign en vue intégration d...herbelin
1999-12-01 - Typing -> Safe_typingfilliatr
1999-11-26ajouts divers pour module Printerfilliatr
1999-11-24MAJ pour fusion avec pretypingherbelin
1999-08-26environnement surfilliatr
1999-08-26 - abstractionfilliatr
1999-08-24mach et himsg; typage sans extractionfilliatr
1999-08-20machine: execute = typage avec universfilliatr
1999-08-17generic, term et evdfilliatr
1999-08-16ancien names decoupe en names + signfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 17:55:04 +0000