aboutsummaryrefslogtreecommitdiff
path: root/pretyping/rawterm.mli
AgeCommit message (Expand)Author
2002-12-21Légère amélioration des messages d'erreur des with-bindings et des Rewriteherbelin
2002-12-09Ajout Simpl et Change sur des sous-termesherbelin
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-10-13Ajout map_rawconstrherbelin
2002-10-12Restriction sur la forme des Syntactic Definition et re-localisation en fonct...herbelin
2002-09-03pretyping/pretyping.mlherbelin
2002-08-02Modules dans COQ\!\!\!\!coq
2002-05-30Finalement un seul constr pour l'instant dans ExtraRedExprherbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-04-11Deuxième passe sur la localisation des messages d'erreurs sur les evars non ...herbelin
2002-04-10Amélioration des messages d'erreurs concernant l'inférence des implicitesherbelin
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-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
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-12-10Suppression Rel de rawconstr et correction de bugs d'affichageherbelin
1999-12-01Intégration du Termast et du Retyping de HH, et modifications connexesherbelin
1999-11-30inductive_key et constructor_keyherbelin
1999-11-29portage Astterm (partiellement)filliatr
1999-11-24MAJ pour fusion avec pretypingherbelin
1999-11-24Version initialeherbelin