aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/sign.ml
Commit message (Expand)AuthorAge
* 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
* ajouts divers pour module PrinterGravatar filliatr1999-11-26
* MAJ pour fusion avec pretypingGravatar herbelin1999-11-24
* environnement surGravatar filliatr1999-08-26
* - abstractionGravatar filliatr1999-08-26
* mach et himsg; typage sans extractionGravatar filliatr1999-08-24
* machine: execute = typage avec universGravatar filliatr1999-08-20
* generic, term et evdGravatar filliatr1999-08-17
* ancien names decoupe en names + signGravatar filliatr1999-08-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 01:50:22 +0000