aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/rawterm.ml
Commit message (Expand)AuthorAge
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)Gravatar herbelin2003-03-29
* *** empty log message ***Gravatar barras2003-03-21
* Légère amélioration des messages d'erreur des with-bindings et des RewriteGravatar herbelin2002-12-21
* Ajout Simpl et Change sur des sous-termesGravatar herbelin2002-12-09
* Ajout de Cases dans abbreviatable constr (aconstr) [utilisé dans laGravatar herbelin2002-11-18
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Ajout map_rawconstrGravatar herbelin2002-10-13
* Restriction sur la forme des Syntactic Definition et re-localisation en fonct...Gravatar herbelin2002-10-12
* pretyping/pretyping.mlGravatar herbelin2002-09-03
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Finalement un seul constr pour l'instant dans ExtraRedExprGravatar herbelin2002-05-30
* 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