aboutsummaryrefslogtreecommitdiff
path: root/kernel/sign.mli
AgeCommit message (Expand)Author
2013-04-29Merging Context and Sign.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2012-12-14Modulification of identifierppedrot
2012-08-08Updating headers.herbelin
2011-07-29Environ: generic equality on named_context replaced by named_context_equalpuech
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-04-29Various minor improvements of comments in mli for ocamldocletouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2008-12-31Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->herbelin
2006-09-01Ajout iter_rel_context/iter_named_contextherbelin
2005-02-18Added map_named_contextherbelin
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-02-22suppression de pop_namedbarras
2002-02-14- Reforme de la gestion des args recursifs (via arbres reguliers)barras
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-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
2001-03-15entetesfilliatr
2001-02-14Mise en place d'un système optionnel de discharge immédiat; prise en compte...herbelin
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
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-25retablissement make doc et make minicoqfilliatr
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-05-05docherbelin
2000-04-21Sign.db_signature is now an abstract typecourant
2000-01-28documentationfilliatr
2000-01-27erreurs latex dans interfacesfilliatr
2000-01-26MAJ ocaml 2.99 (espaces dans la syntaxe des cast)herbelin
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-09-19 - un effort sur la doc (ocamlweb)filliatr
1999-08-30un petit effort de presentation dans les interfacesfilliatr
1999-08-26environnement surfilliatr
1999-08-24mach et himsg; typage sans extractionfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:56:22 +0000