aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/class.ml
Commit message (Expand)AuthorAge
* Mieux à sa place dans toplevelGravatar herbelin2000-11-20
* Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ...Gravatar herbelin2000-11-06
* nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...Gravatar filliatr2000-11-06
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage AppL en AppGravatar herbelin2000-10-01
* Disparition du type oper mais nouveau type global_referenceGravatar herbelin2000-10-01
* Abstraction de constrGravatar herbelin2000-09-14
* Modification mkAppL; abstraction via kind_of_term; changement dans ReductionGravatar herbelin2000-09-12
* Correction pour make docGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* reparation bug des coercions (cas ou on importe une coercion faisantGravatar barras2000-08-08
* Mise en place d'un choix constr/typed_type en remplacement de certains CastGravatar herbelin2000-06-01
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
* Ajout de RecordGravatar herbelin2000-01-11
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 06:10:07 +0000