aboutsummaryrefslogtreecommitdiff
path: root/parsing/prettyp.ml
AgeCommit message (Collapse)Author
2006-05-23Nouvelle implantation du polymorphisme de sorte pour les familles inductivesherbelin
- prise en compte du niveau à la déclaration du type comme une fonction des sortes des conclusions des paramètres uniformes - suppression du retypage de chaque instance de type inductif (trop coûteux) et donc abandon de l'idée de calculer une sorte minimale même dans des cas comme Inductive t (b:bool) := c : (if b then Prop else Type) -> t. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8845 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-27Standardisation nom option_app en option_mapherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8752 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-28Correction bug Inspect introduit par le passage du discharge à une méthode ↵herbelin
associée aux objects git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7938 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Restructuration et simplification des fonctions d'affichage, de détypageherbelin
et d'"externalisation"; standardisation du nom des fonctions d'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7837 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-26Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des ↵herbelin
G_*new en G_*.ml + autres petites modifications liées à suppression du traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7740 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur ↵herbelin
(mécanismes de renommage des noms de constantes, de module, de ltac et de certaines variables liées de lemmes et de tactiques, mécanisme d'ajout d'arguments implicites, etc.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7732 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-21Correction bug dé-globalisation syntactic def (cf coq-club 20/11/05)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7596 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par ↵herbelin
ocaml 3.09 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-02Types inductifs parametriquesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7493 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-19pas besoin de List.length pour savoir si une liste est videletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7306 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-20Keep ClosedSection marker for resetherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6758 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Renaming Print Canonical Structure into Print Canonical Projectionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6750 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-12Nouvelle mouture Print Canonical Structuresherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6714 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-12Ajout Print Canonical Structuresherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6711 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-14Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedsacerdot
to accept a mind_specif (a couple mutual_inductive_body * one_inductive_body) instead of looking it up in the environment. A version of the same functions with the old type is put in Inductiveops (outside the kernel). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6589 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-13Amélioration message Locateherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6583 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-02Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de ↵herbelin
printers dans ocamldebug git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6546 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-09Amélioration message localisation constructions et modulesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6453 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-16IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).sacerdot
MOVITATION: in a forthcoming commit the application of a substitution to a constant will return a constr and not a constant. The application of a substitution to a kernel_name will return a kernel_name. Thus "constant" should be use as a kernel name for references that can be delta-expanded. KNOWN PROBLEMS: the only problem faced is in pretyping/recordops.ml (the code that implements "Canonical Structure"s). The ADT is violated once in this ocaml module. My feeling is that the implementation of "Canonical Structure"s should be rewritten to avoid this situation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6303 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03premiere reorganisation de l\'unificationbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-03Affichage de l'opacité par About mais pas par Print (compatibilité coq'art)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5802 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-02Affichage de l'opacité dans Print et Aboutherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5793 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-02Correction oubli du cas pas d'arguments implicites du toutherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5414 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-28Expansion du type par nécessité dans le cas d'affichage d'implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5398 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-29Réutilisation de VernacSyntacticDefinition pour différencier "Notation id ↵herbelin
:= c" de "Notation "'id'" := c" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5264 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-15Ajout Print Implicit avec depliage du typeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4919 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-23Saut de ligne avant les infos non logiques de print_aboutherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4714 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-21Extension de Locateherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4688 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-13Ameliration affichage inductifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4615 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-11Ajout fnl() dans Aboutherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4599 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-07Inspect saute maintenant les marqueurs invisiblesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4535 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-26Bug aboutherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4492 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-26Ajout 'About'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4484 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-21Mise en place d'implicites par noms en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4430 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Affichage des scopes d'argumentsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4376 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-05Impression sans ',' des constructeurs de meme type, pour v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4301 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-31Affichage des inductifs en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4281 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-08Tables logarithmiques pour les coercions + nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4103 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Réorganisation de Impargs + mise en place d'une infrastructureherbelin
(notatemment des tables de parsing et d'affichage différenciées) permettant au traducteur de changer les implicites git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3874 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-12*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-27Nouvelle syntaxe style 'Inductive color : Set := black, blue, white : ↵herbelin
color' pour les types énumérés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3716 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-31Pour satisfaire ProofGeneralcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3634 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-27Deux p\'tits trucs ;)coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3614 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-19Petit netoyage dans libcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3463 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-13possibilité de faire Print M avec M module ou modtype au lieu de Print ↵letouzey
Module et Print Module Type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3430 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-03la table PARAMETER n'existe plus (mergé dans la table CONSTANT)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3369 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Réaffichage des Syntactic Definition (printer constr_expr).herbelin
Affinement de la gestion des niveaux de constr. Cablage en dur du parsing et de l'affichage des délimiteurs de scopes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3295 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-14Réforme de l'interprétation des termes :herbelin
- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-05Intégration des modifs de la branche mowgli :herbelin
- Simplification de strength qui est maintenant un simple drapeau Local/Global. - Export des catégories de déclarations (Lemma/Theorem/Definition/.../ Axiom/Parameter/..) vers les .vo (nouveau fichier library/decl_kinds.ml). - Export des variables de section initialement associées à une déclaration (nouveau fichier library/dischargedhypsmap.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3212 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 13:12:26 +0000