aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/retyping.mli
Commit message (Expand)AuthorAge
* Compatibilité du polymorphisme de constantes avec les sections.Gravatar herbelin2006-10-29
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
* - Indtypes: en attente opinion CoRN, les occurrences de Type non explicitesGravatar herbelin2006-05-28
* Inductifs avec polymorphisme de sorte (version initiale)Gravatar herbelin2006-03-29
* hiding the meta_map in evar_defsGravatar barras2004-09-15
* Nouvelle en-têteGravatar herbelin2004-07-16
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* Suppression des local_constraints, des ctxtty et du focus.Gravatar clrenard2001-11-06
* Nouvelle fonction get_sort_family_of pour calculer la famille dans lequel vit...Gravatar herbelin2001-09-19
* entetesGravatar filliatr2001-03-15
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage mk_unsafe_judgment en get_judgment_of; ajout get_assumption_ofGravatar herbelin2000-06-29
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* documentationGravatar filliatr2000-01-28
* Nouveaux types 'constructor' et 'inductive' dans Term;Gravatar herbelin1999-12-15
* Ajout des messages d'erreurs de CasesGravatar herbelin1999-12-09
* - global_reference traite des variablesGravatar filliatr1999-12-03
* Retour dans pretypingGravatar herbelin1999-12-01
* déplacé dans kernelGravatar herbelin1999-12-01
* - environment -> safe_environmentGravatar filliatr1999-12-01
* Version initialeGravatar herbelin1999-11-26