aboutsummaryrefslogtreecommitdiff
path: root/library/indrec.mli
AgeCommit message (Expand)Author
2001-11-05GROS COMMIT:barras
2001-09-19Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles de...herbelin
2001-09-10Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ...herbelin
2001-05-23amelioration des messages d'erreurs vis a vis des evarsbarras
2001-03-15entetesfilliatr
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
2000-06-01Mise en place d'un choix constr/typed_type en remplacement de certains Castherbelin
2000-05-22Suite restructuration inductifs; changement nom module Constant en Declarationsherbelin
2000-05-18Adaptation pour nouveaux inductifs (cf Inductive)herbelin
2000-03-21Nettoyageherbelin
2000-03-21Prise en compte nouveau case_infoherbelin
2000-01-07Correction pbs liés aux evarherbelin
1999-12-15Nouveaux types 'constructor' et 'inductive' dans Term;herbelin
1999-12-01 - environment -> safe_environmentfilliatr
1999-11-27fin Recordops, et debut Evarutilfilliatr
1999-11-26Déplacement fonction transform_rec vers pretypingherbelin
1999-11-23modules Indrec, Tacentries, Hiddentacfilliatr
1999-11-22modules Indrec, Wcclausenv; progression dans Tacticalsfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 16:16:03 +0000