aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Collapse)AuthorAge
* Suggestion of additional syntax for intro patterns: Gravatar letouzey2007-07-06
| | | | | | | | | | | | | intros {A,B,C,D} means: intros (A,(B,(C,D))) Should be especially useful when breaking existential hypthesis like {n:nat | P n /\ Q n /\ R n }, hence the notation {}. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9948 85f007b7-540e-0410-9357-904b9bb8a0f7
* Factorisation des types dans l'affichage des paramètres des (Co)Inductif/RecordGravatar herbelin2007-06-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9918 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Ajout de la possibilité d'utiliser la notation Record pour lesGravatar herbelin2007-06-30
| | | | | | | | | | coinductifs à un constructeur (suggestion de Georges). - Si pas de sorte ou arité mentionnée dans Inductive/CoInductive/Record, Type est utilisé comme défaut. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9917 85f007b7-540e-0410-9357-904b9bb8a0f7
* killing some more non-exhaustive patternsGravatar letouzey2007-06-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9912 85f007b7-540e-0410-9357-904b9bb8a0f7
* Corrections dans le Print Assumption. Les definitions locales ("Let") Gravatar aspiwack2007-05-30
| | | | | | | | | | | | sont maintenant prises en compte (ca a l'air de marcher). En plus j'ai corrige l'ordre d'impression pour que ca imprime les noms dans l'ordre alphabetique (avant c'etait l'ordre inverse, etonnament perturbant). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9873 85f007b7-540e-0410-9357-904b9bb8a0f7
* Corrected the treatment of negative numbers for the bigZ parser. And Gravatar aspiwack2007-05-29
| | | | | | | | corrected a small typo in an error message (bogN instead of bigN). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9870 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réaffichage des Structure/Record sous la forme RecordGravatar herbelin2007-05-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9864 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification of VernacScheme to handle a new scheme: Equality (equality inGravatar vsiles2007-05-25
| | | | | | | | | | | | | | | | | boolean, will be added later) and update so everything is fine with the new syntax. New Type: type scheme = | InductionScheme of bool * lreference * sort_expr | EqualityScheme of lreference ... | VernacScheme of (lident * scheme) list git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9860 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added Z and Q implementations with int31.Gravatar aspiwack2007-05-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9846 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Propagation des evars non résolues vers les with_bindings; permet par exempleGravatar herbelin2007-05-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | de résoudre des buts comme celui-ci : Record nat_retract : Type := {f1 : nat -> nat; f2 : nat -> nat; f1_o_f2 : forall x, f1 (f2 x) = x}. Goal nat_retract. exists (fun x => x) (fun x => x). - Nouvelle tentative d'utilisation des types des metas/evars pour inférer de nouvelles instances de metas/evars; permet par exemple d'utiliser f_equal sans option with, mais aussi, avec la modif précédente, de résoudre des buts tels que Goal exists f:bool->Prop, f true = True. exists (fun x => True). [Les expériences passées avaient montré qu'en prenant en compte les types dans l'unification, on peut unifier trop tôt une evars à une mauvaise sorte; à défaut de mécanisme de prise en compte des problème d'unification avec sous-typage, on s'est interdit ici d'unifier des types qui sont des arités.] - Tout les constr de tactic_expr deviennent des open_constr (même si seul with_bindings les accepte au final... c'est pas l'idéal). - Renommage env -> evd et templenv -> env dans clausenv. - Renommage closed_generic_argument -> typed_generic_argument. - Renommage closed_abstract_argument_type -> typed_abstract_argument_type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9842 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du pretty-printing des big-int (la sous-fonction get_height Gravatar aspiwack2007-05-15
| | | | | | | | | faisait n'importe quoi). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9825 85f007b7-540e-0410-9357-904b9bb8a0f7
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
| | | | | | | | | details). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte réversibilité des notations de la forme "Notation Nil := ↵Gravatar herbelin2007-05-10
| | | | | | | | | | @nil". Ajout @ref au niveau constr pour allègement syntaxe. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9819 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveaux changements autour des implicites (notamment suite àGravatar herbelin2007-05-06
| | | | | | | | | | | | | discussion avec Georges) - La notion d'insertion maximale n'est plus globale mais attachée à chaque implicite - Correction de petits bugs dans le calcul des implicites - Raffinement de la notion "sous contexte" pour l'affichage des coercions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9817 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite commit 9810Gravatar herbelin2007-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9811 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout possibilité d'options à trois mots.Gravatar herbelin2007-04-29
| | | | | | | | | | Suppression au passage syntaxe "Set table field ref", synonyme de "Add table field ref" et de "Unset table field ref", synonyme de "Remove table field ref". Changement de la syntaxe "Test tabel field val" en ""Test tabel field for val". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9810 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de la possibilité de faire référence dans certains cas à un nomGravatar herbelin2007-04-28
| | | | | | | | | par sa notation (p.ex. pour unfold ou pour lazy delta). Ex: Goal 3+4 = 7. unfold "+". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9804 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.Gravatar herbelin2007-04-28
| | | | | | | | | Fusion des syntaxes de "apply" et "eapply". Ajout de "eapply in", "erewrite" et "erewrite in". Correction au passage des bugs #1461 et #1522). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9802 85f007b7-540e-0410-9357-904b9bb8a0f7
* fin des conclusions multiplesGravatar corbinea2007-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9796 85f007b7-540e-0410-9357-904b9bb8a0f7
* New keyword "Inline" for Parameters and Axioms for automatic Gravatar soubiran2007-04-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | delta-reduction at fonctor application. Example: Module Type S. Parameter Inline N : Set. End S. Module F (X:S). Definition t := X.N. End F. Module M. Definition N := nat. End M. Module G := F M. Print G.t. G.t = nat : Set git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9795 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveau déplacement de constr, cette fois au niveau 8. En fait, il y aGravatar herbelin2007-04-11
| | | | | | | | | | | | | | | | | | | | | | | un problème dû à la non réversibilité de la suppression de règles camlp4 vis à vis de l'insertion : lorsqu'un niveau existant vide est étendu, la suppression non seulement efface l'extension mais aussi le niveau lui-même. Ceci a un effet sur les niveaux vides 8 et 99. Nous n'avons pas trouvé de bonne solution à ce problème et l'utilisation d'extensions aux niveaux 99 ou 8 (anciennement 5 avant ce commit) continue de corrompre le parser si effectuées à l'intérieur de section ou de modules. Voici un exemple montrant le problème : Print Grammar constr. (* le niveau "8" existe *) Section A. Notation "{{ x }}" := (S x) (at level 8). End A. Print Grammar constr. (* le niveau "8" n'existe plus *) Goal True. apply I. (* appelle le niveau constr qui continue d'appeler "8"... échec *) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9756 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remontée de constr de 1 à 5 (pour permettre des notations entre 1 et 5Gravatar herbelin2007-04-10
| | | | | | | tout en évitant que les .. soient dans constr) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9755 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place d'un rafinement de compute. Gravatar jforest2007-04-05
| | | | | | | | | | On peut desormais utiliser: compute delta [f g ...] pour cbv beta iota zera delta [f g ...] et compute delta - [f g ...] pour cbv beta iota zera delta - [f g ...] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9749 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension to the general sequence operator (tactical). Now in addition to ↵Gravatar emakarov2007-04-02
| | | | | | | | | | | the form expr_0 ; [ expr_1 | ... | expr_n ] where expr_i could be empty, expr_i may be ".." or "expr ..". Note that "..." is a part of the metasyntax while ".." is a part of the object syntax. It may be necessary to enclose expr in parentheses. There may be at most one expr_i ending with "..". The number of expr_j not ending with ".." must be less than or equal to the number of subgoals generated by expr_0. The idea is that if expr_i is "expr .." or "..", then the value of expr (or idtac in case "..") is applied to as many intermediate subgoals as necessary to make the number of tactics equal to the number of subgoals. More precisely, if expr_0 generates n subgoals then the command expr_0; [expr_1 | ... | expr_i .. | ... | expr_m], where 1 <= i <= m, applies (the values of) expr_1, ..., expr_{i-1} to the first i - 1 subgoals, expr_i to the next n - m + 1 subgoals, and expr_{i+1}, ..., expr_m to the last m - i subgoals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9742 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des sauts de lignes superflus de Show Script ↵Gravatar notin2007-03-21
| | | | | | (test-suite/output/Tactics.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9725 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a parameter to QuestionMark evar kind to say it can be turned into an ↵Gravatar msozeau2007-03-19
| | | | | | | | | | obligations (even an opaque one). Change cast_type to include the converted-to type or nothing in case of a Coerce cast, required much minor changes. Various little subtac changes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9718 85f007b7-540e-0410-9357-904b9bb8a0f7
* Une passe sur les warnings (ajout Options.warn déclenchée par ↵Gravatar herbelin2007-02-24
| | | | | | | | | compile-verbose + ajout Pp.strbrk pour faciliter les césures faciles + messages divers). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9679 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression d'un résidu de la syntaxe v7 (Print Grammar avec univ)Gravatar herbelin2007-02-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9677 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add 'dest obj as pat in body' keyword as a pattern-matching shortcut.Gravatar msozeau2007-02-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9655 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réintroduction de l'entrée "integer" dans ltac (apparemment disparue lorsGravatar herbelin2007-02-15
| | | | | | | du passage de l'ancienne à la nouvelle syntaxe) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9650 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé deGravatar herbelin2007-02-13
| | | | | | | | fonctionner entre la V7.3 et la V8.0 (notation : "@ ?meta id1 ... idn") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9644 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de code mortGravatar notin2007-02-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9582 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abbreviation of order notation.Gravatar msozeau2007-02-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9576 85f007b7-540e-0410-9357-904b9bb8a0f7
* redirection of errors in coqide + dynamic warning printer (needed for tm_egg)Gravatar corbinea2007-01-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9566 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix order of wf and measure arguments, patch Program doc.Gravatar msozeau2007-01-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9561 85f007b7-540e-0410-9357-904b9bb8a0f7
* "suffices" implemented + syntax cleanupGravatar corbinea2007-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9549 85f007b7-540e-0410-9357-904b9bb8a0f7
* decl mode: anonymous factsGravatar corbinea2007-01-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9534 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1315:Gravatar notin2007-01-22
| | | | | | | | | | | | | | | | | | - ajouts des opérations clear_evar_hyps_in_evar, clear_evar_hyps_in_constr et clear_evar_hyps dans Evarutil, qui permettent de supprimer des hypothèses dans le contexte des evars, en créant une nouvelle evar avec un contexte restreint; - adaptation de clear_hyps dans Logic pour qu'elle mette à jour le contexte des evars; - adaptation de prim_refiner pour qu'elle renvoie le evar_map modifié; - déplacement de la tactique Change_evars dans prim_rule. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9518 85f007b7-540e-0410-9357-904b9bb8a0f7
* changes in declarative language : by term using tacticGravatar corbinea2007-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9512 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petit oubli dans commit 9474Gravatar herbelin2007-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9480 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merge from Lionel Elie Mamane's private branch:Gravatar lmamane2007-01-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | - Makefile: Option (environment variable NO_RECOMPILE_LIB) to not recompile the whole standard library just because the coq binaries got rebuilt. - Infrastructure to change the object pretty-printers at runtime. - Use that infrastructure to make coqtop-protocol with Pcoq trees and Pcoq-protocol with pretty-printed terms possible in coq-interface. - Make "Back(track)" into closed sections, modules and module types "Just Work™". - Modernise/generalise Pcoq protocol a bit, make some of its warts optional. - Implement "Show." in Pcoq mode. - Add Rpow_def.vo to REALSBASEVO so that its dependencies are computed (and used). - "make revision" now handles GNU Arch / tla in addition to svn. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9476 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle approche pour le discharge modulaireGravatar herbelin2007-01-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Avant : une unique méthode discharge_function qui avait accès à l'ancien environnement mais pas de possibilité de raisonner avec les objets du nouvel environnement en cours de construction. C'était problématique pour le discharge des implicites, arguments scope, etc qui étaient finalement faits en même temps que le discharge des constantes et inductifs mais avec pour effets de bord que les entrées dans la lib_stk arrivaient juste avant celles des constantes et inductifs avec des problèmes pour effacer les bonnes entrées au moment du reset - Maintenant : deux méthodes distinctes : discharge_function qui est appliquée pour collecter de l'ancien environnement ce qui est à garder dans la section et rebuild_function qui reconstruit le nouvel environnement connaissant déjà les nouvelles valeurs des objets précédants (on se rapproche ainsi plus de la méthode en deux temps d'avant la 8.1 tout en offrant l'extensibilité que la méthode ancienne du fichier discharge.ml ne permettait pas) Au passage, ajout d'un modificateur Global aux déclarations d'implicites et d'arguments scopes pour indiquer qu'elles doivent perdurer à la sortie de la section Au passage, suppression de l'objet DISCHARGED-HYPS-MAP et intégration aux objets VARIABLE/CONSTANT/INDUCTIVE (seule la table des hyps discharged reste) Au passage, nettoyage impargs.ml, suppression code mort résiduel du traducteur etc... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9474 85f007b7-540e-0410-9357-904b9bb8a0f7
* Addition of a "Combined Scheme" vernacular command for building the ↵Gravatar msozeau2006-12-23
| | | | | | | | | conjunction of mutual inductions principles. e.g: Combined Scheme mutind from tree_ind, forest_ind gives a conclusion (forall t : tree, P t) /\ (forall f : forest, P0 f). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9461 85f007b7-540e-0410-9357-904b9bb8a0f7
* nouvelle indentation des scriptsGravatar barras2006-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9443 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement dans le kernel : Gravatar bgregoir2006-12-11
| | | | | | | | | | | | | | | | | | | | | - essai de suppression des dependances debiles. (echec) - Application des patch debian. Pour ring et field : - introduciton de la function de sign et de puissance. - Correction de certains bug. - supression de ring_replace .... Pour exact_no_check : - ajout de la tactic : vm_cast_no_check (t) qui remplace "exact_no_check (t<: type of Goal)" (cette version forcais l'evaluation du cast dans le pretypage). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9427 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite ajout option -output-contextGravatar herbelin2006-12-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9416 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une option -output-context qui affiche le contexte en CCI pur à laGravatar herbelin2006-12-08
| | | | | | | sortie de session (nécessite option -batch) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9414 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement de la dépendance de G_vernac en G_constr (sourceGravatar herbelin2006-12-03
| | | | | | | | d'incohérences dans les dépendances en l'absence de g_constr.mli) par une dépendance en Topconstr git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9409 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction boucle du parseur en cas de caractÃère non unicodeGravatar herbelin2006-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9394 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression du type 'tac dans les abstract_argument_type: devenu inutile Gravatar herbelin2006-11-20
| | | | | | | | suite à l'adoption du modèle rlevel,glevel,tlevel et au passage des wit_tactic en types créés dynamiquement (révisions 8917 et 8926). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9393 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-30 21:38:16 +0000