aboutsummaryrefslogtreecommitdiff
path: root/pretyping/retyping.mli
AgeCommit message (Expand)Author
2001-11-06Suppression des local_constraints, des ctxtty et du focus.clrenard
2001-09-19Nouvelle fonction get_sort_family_of pour calculer la famille dans lequel vit...herbelin
2001-03-15entetesfilliatr
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
2000-10-18Simplifications autour de typed_type (renommé types par analogie avec sorts)...herbelin
2000-06-29Renommage mk_unsafe_judgment en get_judgment_of; ajout get_assumption_ofherbelin
2000-05-03Ajout du langage de tactiquesdelahaye
2000-01-28documentationfilliatr
1999-12-15Nouveaux types 'constructor' et 'inductive' dans Term;herbelin
1999-12-09Ajout des messages d'erreurs de Casesherbelin
1999-12-03 - global_reference traite des variablesfilliatr
1999-12-01Retour dans pretypingherbelin
1999-12-01déplacé dans kernelherbelin
1999-12-01 - environment -> safe_environmentfilliatr
1999-11-26Version initialeherbelin