aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/rawterm.ml
Commit message (Expand)AuthorAge
...
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* Deuxième passe sur la localisation des messages d'erreurs sur les evars non ...Gravatar herbelin2002-04-11
* Amélioration des messages d'erreurs concernant l'inférence des implicitesGravatar herbelin2002-04-10
* GROS COMMIT:Gravatar barras2001-11-05
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* Ajout de dynamiques pour les quotations constr et tacticGravatar delahaye2001-10-02
* Facilites pour le debogguage des univers.Gravatar coq2001-05-29
* entetesGravatar filliatr2001-03-15
* Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisationGravatar herbelin2001-03-11
* uniformisation avec constr des lieurs dans rawterm/patternGravatar herbelin2001-02-14
* Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refGravatar herbelin2001-02-07
* Bug localisation des Syntactif DefinitionGravatar herbelin2001-01-31
* Utilisation de global_reference dans rawconstrGravatar herbelin2000-11-20
* merge_locGravatar herbelin2000-11-08
* Déplacement 'a reference et binder_kind de Term vers RawtermGravatar herbelin2000-10-01
* Modification messages d'erreurs, possibilité de n'importe quel constr dans l...Gravatar herbelin2000-05-26
* Bug redondance entre 'RRef (RMeta _)' et 'PMeta _'Gravatar herbelin2000-05-02
* Déplacement du type reference dans TermGravatar herbelin2000-04-28
* Changement de représentation du contexte des réf dans rawconstr et patternGravatar herbelin2000-04-28
* Introduction d'un type constr_pattern pour les différents filtragesGravatar herbelin2000-04-26
* Prise en compte nouveau case_infoGravatar herbelin2000-03-21
* Quelques fonctions sur les locations des rawconstrGravatar herbelin1999-12-11
* Version initialeGravatar herbelin1999-11-24
* Type ML des termes non prétypésGravatar herbelin1999-10-24