aboutsummaryrefslogtreecommitdiff
path: root/pretyping/rawterm.ml
AgeCommit message (Expand)Author
2001-11-05GROS COMMIT:barras
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
2001-10-02Ajout de dynamiques pour les quotations constr et tacticdelahaye
2001-05-29Facilites pour le debogguage des univers.coq
2001-03-15entetesfilliatr
2001-03-11Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisationherbelin
2001-02-14uniformisation avec constr des lieurs dans rawterm/patternherbelin
2001-02-07Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refherbelin
2001-01-31Bug localisation des Syntactif Definitionherbelin
2000-11-20Utilisation de global_reference dans rawconstrherbelin
2000-11-08merge_locherbelin
2000-10-01Déplacement 'a reference et binder_kind de Term vers Rawtermherbelin
2000-05-26Modification messages d'erreurs, possibilité de n'importe quel constr dans l...herbelin
2000-05-02Bug redondance entre 'RRef (RMeta _)' et 'PMeta _'herbelin
2000-04-28Déplacement du type reference dans Termherbelin
2000-04-28Changement de représentation du contexte des réf dans rawconstr et patternherbelin
2000-04-26Introduction d'un type constr_pattern pour les différents filtragesherbelin
2000-03-21Prise en compte nouveau case_infoherbelin
1999-12-11Quelques fonctions sur les locations des rawconstrherbelin
1999-11-24Version initialeherbelin
1999-10-24Type ML des termes non prétypésherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:03:10 +0000