aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/termast.ml
Commit message (Expand)AuthorAge
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Utilisation d'une construction spéciale SECVAR pour gérer laGravatar herbelin2002-05-14
* Correction bug infix sur des varaiablesGravatar mohring2002-03-29
* petit nettoyage de kernel/inductiveGravatar barras2002-02-07
* MAJ de la traduction en ast des variables de section en qualidGravatar herbelin2001-12-13
* compat ocaml 3.03Gravatar filliatr2001-12-13
* GROS COMMIT:Gravatar barras2001-11-05
* Abstraction de l'immplementation de dirpath et implementation dans l'autre se...Gravatar herbelin2001-10-17
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* Ajout de dynamiques pour les quotations constr et tacticGravatar delahaye2001-10-02
* ParsingGravatar herbelin2001-08-10
* Facilites pour le debogguage des univers.Gravatar coq2001-05-29
* un warning pas beau supprimméGravatar filliatr2001-04-23
* Bug affichage d'implicites pour les vars lieesGravatar herbelin2001-04-15
* Bug MUTCASE au lieu CASEGravatar herbelin2001-03-22
* entetesGravatar filliatr2001-03-15
* Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisationGravatar herbelin2001-03-11
* Déplacement de qualid dans Nametab, hors du noyauGravatar herbelin2001-03-01
* Bug affichage coercionsGravatar herbelin2001-02-16
* ident au lieu de string pour le nom de base de qualidGravatar herbelin2001-02-16
* Mise en place d'un système optionnel de discharge immédiat; prise en compte...Gravatar herbelin2001-02-14
* Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refGravatar herbelin2001-02-07
* Ajout d'une commande pour afficher chaque coercion à la demandeparsing/g_bas...Gravatar herbelin2001-02-06
* Suppression de l'affichage des instances des ?nGravatar herbelin2000-12-18
* Ajout des Fix et CoFix dans les patternsGravatar delahaye2000-11-28
* Prise en compte des implicites de locaux à l'affichageGravatar herbelin2000-11-27
* Affichage des paths avec des '.'; print_id, print_sp -> pr_id, pr_sp;Gravatar herbelin2000-11-23
* Utilisation de global_reference dans rawconstrGravatar herbelin2000-11-20
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Bug affichage des implicites; bug de compatibilité LAMBDA/LAMBDALISTGravatar herbelin2000-10-05
* Utilisation de local_strong plutôt que strong buggé avec défs localesGravatar herbelin2000-10-04
* Renommage AppL en AppGravatar herbelin2000-10-01
* Abstraction de constrGravatar herbelin2000-09-14
* Correction pour make docGravatar herbelin2000-09-10
* Suppression de AbstGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* portage RefineGravatar filliatr2000-07-20
* Nettoyage de GenericGravatar herbelin2000-05-31
* Modification messages d'erreurs, possibilité de n'importe quel constr dans l...Gravatar herbelin2000-05-26
* Réparation bug d'affichage et affichage des instanciations par des {...}Gravatar herbelin2000-05-23
* CommentairesGravatar herbelin2000-05-22
* suppression de Fw pour les implicitesGravatar herbelin2000-05-03
* Bug redondance entre 'RRef (RMeta _)' et 'PMeta _'Gravatar herbelin2000-05-02
* Suite intégration de constr_patternGravatar herbelin2000-04-30
* 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
* Extension du case_info : ajout du nombre de vrais args de chaque constr pour ...Gravatar herbelin2000-03-21
* Affichage des anonymes si lambdaGravatar herbelin2000-03-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 18:44:10 +0000