aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Collapse)AuthorAge
* Installation des printers de nombres pour constr_exprGravatar herbelin2002-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3268 85f007b7-540e-0410-9357-904b9bb8a0f7
* Les parenthèses de la notation '(n)' maintemant mises par ML pour un ↵Gravatar herbelin2002-11-20
| | | | | | meilleur affichage des entiers dans le scope nat_scope git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3261 85f007b7-540e-0410-9357-904b9bb8a0f7
* Introduction d'un constructeur ARROW; rétablissement priorités desGravatar herbelin2002-11-20
| | | | | | | | arguments de APPTAIL (autre méthode dans g_constr.ml4 pour gérer le conflit entre "(f 3+4)" et "(f 3!x)") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3260 85f007b7-540e-0410-9357-904b9bb8a0f7
* Problème avec le choix d'introduire une indirection vers un rawconstr pourGravatar herbelin2002-11-17
| | | | | | | | | les extensions de grammaire par Grammar; pose p.ex. problème pour la résolution des implicites. Pour l'instant, une rustine pour contourner le problème git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3248 85f007b7-540e-0410-9357-904b9bb8a0f7
* Passage à une représentation des fixpoints plus primitive dans constr_expr ↵Gravatar herbelin2002-11-15
| | | | | | (càd avec indices) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3245 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug factorisation grammaireGravatar herbelin2002-11-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3242 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compatibilité avec les << >> dans la très ancienne syntaxe des actionsGravatar herbelin2002-11-14
| | | | | | | de Grammar. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3240 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug factorisationGravatar herbelin2002-11-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3239 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restauration échappement MLGravatar herbelin2002-11-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3238 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
| | | | | | | | | | | | | | | - 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
* Un hack camlp4 qui marche à tous les coups pour continuer à parser '(n)' ↵Gravatar herbelin2002-11-07
| | | | | | comme un entier de nat git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3222 85f007b7-540e-0410-9357-904b9bb8a0f7
* fix forbidden currified constructorsGravatar ddr2002-11-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3221 85f007b7-540e-0410-9357-904b9bb8a0f7
* Intégration des modifs de la branche mowgli :Gravatar herbelin2002-11-05
| | | | | | | | | | | - 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
* Ajout delimiteurs dans les motifs de CasesGravatar herbelin2002-11-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3203 85f007b7-540e-0410-9357-904b9bb8a0f7
* Désagglutination du squelette de la notation et de sa précédenceGravatar herbelin2002-10-30
| | | | | | | Premier jet pour Print Scope; Print Scopes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3197 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mais laisser la syntaxe (!id) aussi disponible !Gravatar herbelin2002-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3190 85f007b7-540e-0410-9357-904b9bb8a0f7
* Parenthèse non obligatoires autour de !id sans argumentGravatar herbelin2002-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3188 85f007b7-540e-0410-9357-904b9bb8a0f7
* Des critères plus fins d'analyse des implicites automatiques; meilleur ↵Gravatar herbelin2002-10-28
| | | | | | affichage des implicites en cas d'application partielle ou inférence via une position flexible; gestion des implicites en positions terminales pour anticiper sur un implicite dans nil et cie git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3185 85f007b7-540e-0410-9357-904b9bb8a0f7
* Clarification changements autour de Remark/Fact/LocalGravatar herbelin2002-10-23
| | | | | | | Ajout de la syntaxe "Theorem f [binders] : t", comme pour Definition et Local git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3180 85f007b7-540e-0410-9357-904b9bb8a0f7
* Le test de redondance d'une règle était trop fortGravatar herbelin2002-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3177 85f007b7-540e-0410-9357-904b9bb8a0f7
* Redéplacement de + (sum) et * (prod) au niveau de + et * de ↵Gravatar herbelin2002-10-22
| | | | | | l'arithmétique; ajout d'une option 'level' pour Notation; utilisation de Notation pour sumor et sumbool git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3173 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un suffixe "as [ names ]" pour nommer manuellement lesGravatar herbelin2002-10-21
| | | | | | | variables introduites par NewDestruct et NewInduction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3169 85f007b7-540e-0410-9357-904b9bb8a0f7
* NewDestruct/NewInduction acceptent l'option "using"Gravatar herbelin2002-10-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3167 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des délimiteurs dans les motifs de CasesGravatar herbelin2002-10-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3165 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des délimiteurs dans les motifs de CasesGravatar herbelin2002-10-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3164 85f007b7-540e-0410-9357-904b9bb8a0f7
* L'application de ltac attend une référence; meilleure protection contreGravatar herbelin2002-10-14
| | | | | | | les erreurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3141 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout "Arguments Scope" pour associer des "scopes" aux arguments d'uneGravatar herbelin2002-10-14
| | | | | | | référence donnée git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3133 85f007b7-540e-0410-9357-904b9bb8a0f7
* Première proposition d'un type ML exprimant la syntaxe de constr; nettoyageGravatar herbelin2002-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3121 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ↵Gravatar herbelin2002-10-13
| | | | | | hack temporaire autour du printer git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3120 85f007b7-540e-0410-9357-904b9bb8a0f7
* réparation de la protection contre les clauses indiscernables de TACTIC ↵Gravatar herbelin2002-10-12
| | | | | | EXTEND et VERNAC COMMAND EXTEND git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3119 85f007b7-540e-0410-9357-904b9bb8a0f7
* Notation 2:Check et 2:EvalGravatar herbelin2002-10-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3118 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restriction sur la forme des Syntactic Definition et re-localisation en ↵Gravatar herbelin2002-10-12
| | | | | | fonction de l'endroit d'utilisation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3117 85f007b7-540e-0410-9357-904b9bb8a0f7
* Lazy manuelles dans le codeGravatar coq2002-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3100 85f007b7-540e-0410-9357-904b9bb8a0f7
* Lazy experimentale temporaire...Gravatar coq2002-10-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3091 85f007b7-540e-0410-9357-904b9bb8a0f7
* pretty s'appellait prettyp mais il est revenu sous son ancien nomGravatar herbelin2002-10-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3090 85f007b7-540e-0410-9357-904b9bb8a0f7
* passage a ocaml 3.06Gravatar herbelin2002-09-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3041 85f007b7-540e-0410-9357-904b9bb8a0f7
* Un peu (plus) d'ordre dans Nametab...Gravatar coq2002-09-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3031 85f007b7-540e-0410-9357-904b9bb8a0f7
* La notation with dependante + affichage dependante de moduels corrigeGravatar coq2002-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3025 85f007b7-540e-0410-9357-904b9bb8a0f7
* La notation 'with'. L'interpretation - version preliminaireGravatar coq2002-08-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2975 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pretty-printing preliminaire des modules, commandesGravatar coq2002-08-19
| | | | | | | | | | | | | Print Module qid. Print Module Type qid. et affichage pendant Print All. Tout ca est preliminare, seuls les noms des composants sont affiches et non pas les corps... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2973 85f007b7-540e-0410-9357-904b9bb8a0f7
* Strengthenning rules for modules + No modules in sectionsGravatar coq2002-08-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2969 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réparation d'un bug qui considérait les composantes d'un QUALIDGravatar herbelin2002-07-30
| | | | | | | comme occurrences de variables indépendantes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2942 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pb de factorisation camlp4Gravatar herbelin2002-07-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2871 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pour assurer une compatibilite avec la 7.3Gravatar herbelin2002-07-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2870 85f007b7-540e-0410-9357-904b9bb8a0f7
* Généralisation des syntaxes ': T := t', ':= t : T', ': T', ':= t' pourGravatar herbelin2002-07-11
| | | | | | | les définitions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2852 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coercion de la syntaxe des motifs non atomiquesGravatar herbelin2002-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2794 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petits beug d'affichages.Gravatar gregoire2002-06-13
| | | | | | | Benj git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2778 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction mauvais ordre dans le parsing des dirpath; MAJ de la quotificationGravatar herbelin2002-06-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2756 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fusion entre la nouvelle et l'ancienne syntaxe de HintDestructGravatar herbelin2002-06-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2755 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-19 01:35:23 +0000