aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Collapse)Author
2000-10-30Priorite du Try/Orelse + Debug switch + correction bug dans Patterndelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@785 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-26Renommage var en named et decl en assumherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@763 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-24Bug de copier-collerherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@748 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-21Pb affichage warningherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@733 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-18Simplifications autour de typed_type (renommé types par analogie avec ↵herbelin
sorts); documentation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@728 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-18Renommage canonique :herbelin
declaration = definition | assumption mode de reference = named | rel Ex: push_named_decl : named_declaration -> env -> env lookup_named : identifier -> safe_environment -> constr option * typed_type add_named_assum : identifier * typed_type -> named_context -> named_context add_named_def : identifier*constr*typed_type -> named_context -> named_context git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@723 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-18Parsing des motifs de Syntax avec la grammaire associée à l'univers de la ↵herbelin
déclaration (constr, tactic ou vernac) au lieu de ast (comme cela a été fait pour Grammar) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@721 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-182èmeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@720 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-18Mise en place de parseurs avec globalisation pas seulement dans les ↵herbelin
quotations, pour utilisation par les règles de syntaxe et grammaire git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@718 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-18Nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@717 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-18globalize_command devient globalize_constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@716 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-18Correction pb de globalisation dans print_mutualherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@715 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-17Pb factorisation de Print Grammarherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@713 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-16Changement "command" en "constr" et globalize_command en globalize_constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@711 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-11Suite du précédentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@697 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-10Plus d'échec sur les globaux lorsque prterm est appelé par le débuggerherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@678 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-06Correction incompatibilites dans la fn des types des inductifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@673 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-05Bug affichage des implicites; bug de compatibilité LAMBDA/LAMBDALISTherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@658 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-04Utilisation de local_strong plutôt que strong buggé avec défs localesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@652 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-03Ajout castedopenconstrargherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@643 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-03Ajout de globpr dans tacprherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@642 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-03Ajout castedopenconstrarg; Renommage tactique Let en LetTacherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@640 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-03Reorganisation des interp_constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@639 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01Renommage AppL en Appherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@634 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01Disparition du type oper mais nouveau type global_referenceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@620 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01Déplacement 'a reference et binder_kind de Term vers Rawtermherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@619 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-26Nettoyage pretyping; ise_resolve_* devient understand_*; Ajout d'une notion ↵herbelin
de 'OpenConstr' constitué d'un terme avec Métas et d'une liste de types pour les métas git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@615 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-14Abstraction de constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@604 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-12Modification mkAppL; abstraction via kind_of_term; changement dans Reductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@597 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-10Correction pour make docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@594 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-10Suppression de Abstherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@593 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-10Ajout d'un LetIn primitif.herbelin
Abstraction de constr via kind_of_constr dans une bonne partie du code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@591 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-06Canonisation de certains noms dans Pretyping, Asterm et Safe_typingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@586 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-06code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@585 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-08-20Bug dans le filtrage des paires, nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@580 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-08-17Pattern matching de sous-termes + exceptions dans le lexerdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@578 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-28Plus de piquants dans les actions des grammaires; nom de la grammaire pris ↵herbelin
comme parseur par defaut; le type List devient AstList git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@575 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-26Ajout syntaxe [ phr1 ... phrn ]. pour grouper des commandes (pour Time ou ↵herbelin
Grammar) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@574 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-26bug token "<:" et ":<"herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@573 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-25retablissement make doc et make minicoqfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@571 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@568 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-21retablissement minicoq (pour Jacek)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@565 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-21Pattern -> parsingdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@564 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-21Modifs d'interpretation de patterns + exceptions dans le lexerdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@561 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-20portage Refinefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@559 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-01Précalcul de la forme canonique des constructeurs et arités pour traiter ↵herbelin
les cas du fichier Ensemble.v sans avoir à renormaliser à chaque fois git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@548 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-01index devenu list_index échoue maintenant avec Not_found et plus Failureherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@540 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29Renommage mk_unsafe_judgment en get_judgment_ofherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@525 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-21$BINDER -> BINDERfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@517 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-21 - $BINDER -> BINDER dans g_constr.ml4 (=> erreur syntax Fix)filliatr
- suite portage Ring git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@516 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-29 11:25:46 +0000