aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/detyping.ml
Commit message (Expand)AuthorAge
* compat ocaml 3.03Gravatar filliatr2001-12-13
* Bug nommage des fonctions définies par récursion mutuelleGravatar herbelin2001-11-19
* Re-installation de l'affichage des globaux par des noms courtsGravatar herbelin2001-11-19
* GROS COMMIT:Gravatar barras2001-11-05
* Reorganisation de Goption. Passage des options l'utilisant en synchroneGravatar letouzey2001-10-30
* Suppression option immediate_discharge; nettoyage de Declare et conséquencesGravatar herbelin2001-10-11
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* Bug d'affichage du prédicat, bug d'affichage des clauses en présence de dé...Gravatar herbelin2001-10-03
* Réparation des options Set Printing and coGravatar herbelin2001-09-21
* erreur de pretty-print lors de l'affichage de termes avec de Bruijn non liesGravatar barras2001-09-04
* Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...Gravatar herbelin2001-07-21
* Facilites pour le debogguage des univers.Gravatar coq2001-05-29
* Changement de la structure des points fixesGravatar barras2001-05-03
* entetesGravatar filliatr2001-03-15
* Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisationGravatar herbelin2001-03-11
* nouvelle implantation de la reductionGravatar barras2001-03-01
* 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
* Prise en compte du let-in dans lookup_*_as_renamedGravatar herbelin2001-01-30
* Bugs prise en compte du prédicat dans le Cases; le prédicat du Cases devien...Gravatar herbelin2000-12-14
* Utilisation de global_reference dans rawconstr; blindage pour quand appelé d...Gravatar herbelin2000-11-20
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Renommage canonique :Gravatar herbelin2000-10-18
* Bug affichage du nom des letinGravatar herbelin2000-10-11
* Renommage AppL en AppGravatar herbelin2000-10-01
* Abstraction de constrGravatar herbelin2000-09-14
* Modification mkAppL; abstraction via kind_of_term; changement dans ReductionGravatar herbelin2000-09-12
* 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
* Nettoyage de GenericGravatar herbelin2000-05-31
* Modification messages d'erreurs, possibilité de n'importe quel constr dans l...Gravatar herbelin2000-05-26
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
* Effets de bords suite à la restructuration des inductives (cf Inductive)Gravatar herbelin2000-05-18
* Bug redondance entre 'RRef (RMeta _)' et 'PMeta _'Gravatar herbelin2000-05-02
* Changement de représentation du contexte des réf dans rawconstr et patternGravatar herbelin2000-04-28
* N'importe quel rawconstr maintenant dans le contexte d'une référenceGravatar herbelin2000-04-26
* Prise en compte nouveau case_infoGravatar herbelin2000-03-21
* Abstraction de l'implémentation des signatures de Sign en vue intégration d...Gravatar herbelin2000-01-26
* Traduction constr->rawconstr (avant dans TermastGravatar herbelin2000-01-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 12:27:55 +0000