aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* 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
* Correction du bug #1509Gravatar notin2007-05-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9818 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
* Modification syntaxe de TestGravatar herbelin2007-04-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9816 85f007b7-540e-0410-9357-904b9bb8a0f7
* Orthographe en passantGravatar herbelin2007-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9815 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quelques exemples sur l'asymétrie de la conversionGravatar herbelin2007-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9814 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus d'option -v8 dans coqmktopGravatar herbelin2007-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9813 85f007b7-540e-0410-9357-904b9bb8a0f7
* Multiples changements autour des implicites :Gravatar herbelin2007-04-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | - correction du mode strict qui n'était pas si strict, - option "Set Strong Strict Implicit" pour activer le mode strictement strict (désactivé par défaut pour raison de compatibilité), - option "Set Reversible Pattern Implicit" pour activer les implicites inférables par unification-pattern (désactivé par défaut par compatibilité), - option "Unset Printing Implicit Defensive" pour désactiver l'affichage des implicites n'ayant pas été décelés stricts, - option "Set Maximal Implicit Insertion" pour que les applications soient saturées en implicites si possible, - une optimisation du mode non strict pour que l'algo de recherche des implicites renonce à calculer les occurrences non strictes qui pourraient avoir à être affichées dans le mode défensif, avec pour conséquence que le mode défensif, pour celui qui le veut, devient a priori encore plus verbeux, ex: Set Implicit Arguments. Definition id x : nat := x. Parameter f : forall n, id n = id n -> Prop. Check (f (refl_equal O)). (* Affichait: "f (refl_equal 0)" mais affiche maintenant "f (n:=0) (refl_equal 0)" *) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9812 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
* Correction bug #1507 (report révision 9807 de v8.1 vers trunk)Gravatar herbelin2007-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9809 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #1519Gravatar herbelin2007-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9806 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
* Déplacement des opérations sur bool dans l'état initialGravatar herbelin2007-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9803 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
* fixed glitch in escapeGravatar corbinea2007-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9800 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation de Existential et de Show Existential (fixes bug #1294)Gravatar notin2007-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9799 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petite modif dans instantiate_pf_com: ajout de test pour l'indice 0, et ↵Gravatar notin2007-04-26
| | | | | | uniformisation des messages d'erreur wrt instantiate git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9798 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
* (PR#1529)Gravatar soubiran2007-04-25
| | | | | | | | Now the warning will be printed when the flag verbose is on. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9794 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation du nouveau "Unset Elimination Schemes" pour empêcher la création Gravatar herbelin2007-04-25
| | | | | | | des schémas d'élimination standard de JMeq, plutôt que "Reset JMeq_rect". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9793 85f007b7-540e-0410-9357-904b9bb8a0f7
* Le configure et le README accordent leurs violons pour exiger ocaml 3.07 ↵Gravatar herbelin2007-04-24
| | | | | | (restera à accorder les .spec) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9792 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ ppc/i386Gravatar herbelin2007-04-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9791 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1496 (ajout de Program Definition et Program Fixpoint aux ↵Gravatar notin2007-04-23
| | | | | | commandes vernac considérées par Coqdoc) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9790 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed some typos.Gravatar glondu2007-04-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9789 85f007b7-540e-0410-9357-904b9bb8a0f7
* debug plus poussé induction dépendanteGravatar corbinea2007-04-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9787 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Correction d'un bug de make_clenv_binding_apply révélé par le commit 9771Gravatar herbelin2007-04-18
| | | | | | | | | | | (les let-in étaient comptés comme des produits, introduisant une incohérence sur le nombre de produits à instancier dans les lemmes appelés par apply). - Export simplest_eapply pour utilisation dans Sophia/RecursiveDefinition. - Doc développeur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9785 85f007b7-540e-0410-9357-904b9bb8a0f7
* Corrected a LaTeX typo.Gravatar emakarov2007-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9784 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correct implementation of undo in obligations handling code, correct some ↵Gravatar msozeau2007-04-17
| | | | | | | | | bugs in pattern-matching compilation with multiple matched objects. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9783 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reorder hook and printing of message, more natural this way.Gravatar msozeau2007-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9782 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changed many refman/*.tex files. Put \label and \index commands that ↵Gravatar emakarov2007-04-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | immediately follow sectioning commands insides those sectioning commands. If \label{...} is placed after \section{...}, then, when clicking on the link in the HTML file produced by Hevea, we are moved to the correct section, but the section header is just above the screen. Hevea manual recommends writing \section{...\label{...}} and similarly for index. On the other hand, writing commands inside the argument of sectioning commands is potentially dangerous because these arguments are reproduced not only to produce the section header but also to produce headers and/or table of contents entries. Thus, \index{...} and \labels{...} may be executed several times. Indeed, if we put a \typeout{...} instruction inside the argument to a sectioning command then it will be executed, besides the section itself, in the table of contents and once for every appearance of the header. However, it seems that the \label command are not executed several times unless they are prefixed with \protect, and \index command is not executed multiple times even then. So maybe it's OK to put \label and \index inside sectioning commands. When hyperref package is used, the \newlabel command left in .aux file has an extra group {...} which includes another \label command! This may lead to trouble when we use \nameref (?). However, the most reliable way would be to use the optional argument of sectioning commands. Then the text only goes to the optional argument and the text plus \label plus \index goes to the main argument. The optional argument is used for headers and table of contents. This works fine with Hevea as well. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9781 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added the option to set/unset the automatic generation of elimination schemesGravatar vsiles2007-04-17
| | | | | | | | Set Elimination Schemes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9780 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rajout du mot Fix dans le printerGravatar vsiles2007-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9779 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retablissement de Fix dans print_pure_constr Gravatar vsiles2007-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9778 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1510Gravatar notin2007-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9777 85f007b7-540e-0410-9357-904b9bb8a0f7
* Export de simplest_eapply, utilisé dans la contrib interfaceGravatar notin2007-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9776 85f007b7-540e-0410-9357-904b9bb8a0f7
* fix bug with dependent inductive familiesGravatar corbinea2007-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9775 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add the possibility to change the position of tabs in main window (from r9717).Gravatar glondu2007-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9774 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix a bug which sometimes made coqide crash after changingGravatar glondu2007-04-16
| | | | | | | preferences (first fixed in rev. 9716). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9773 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed from headers.hva the code to make index point to the sectionGravatar emakarov2007-04-16
| | | | | | | | | labels and not other environment labels (such as enumerate or theorem). This facility was added to Hevea, which is available at http://hevea.inria.fr/distri/unstable/hevea-2007-04-16.tar.gz git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9772 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite unification apply et eapply (l'un et l'autre profite maintenantGravatar herbelin2007-04-16
| | | | | | | | | | de la réduction paresseuse du lemme [eapply n'en profitait pas], et l'un et l'autre profite de l'unification2nd ordre sur la forme réduite du lemme [apply n'en profitait pas]). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9771 85f007b7-540e-0410-9357-904b9bb8a0f7
* Essai de partage de code entre apply et eapplyGravatar herbelin2007-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9770 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un test de complexité de injection (cf bug 1173)Gravatar herbelin2007-04-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9769 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite du commit 9760 : l'uniformisation du comportement de one_step_reduce,Gravatar herbelin2007-04-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | reduce_to_ind et reduce_to_ref a révélé que ceux-ci pouvaient contourner l'opacité des constantes lorsque celles-ci apparaissaient comme argument d'un match ou d'un fix (et ce depuis la V5.10 environ). Exemple: Definition f (A B:Set) := pair A B. Opaque f. Goal fst (f unit unit) -> True. intro H. destruct H. (* bypassed opacity *) Definition f (A:Set) := A. Opaque f. Goal (f unit) -> True. intro H. destruct H. (* didn't bypass opacity *) Contourner le statut Opaque quand on recherche un inductif (ce qui est le rôle de reduce_to_ind) ne paraît pas problématique (et il se trouve d'ailleurs que CoRN/ftc/TaylorLemma.v en profitait). Ce contournement de l'opacité a donc été généralisé au cas de constantes arrivant en tête sans être argument d'un match ou d'un fix. Contourner le statut Opaque quand on recherche une constante particulière (ce qui est le rôle général de reduce_to_ref qui est maintenant le seul à reposer sur one_step_reduce) paraît en revanche plus douteux. Plus de contournement d'opacité pour reduce_to_ref donc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9768 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #1499Gravatar notin2007-04-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9767 85f007b7-540e-0410-9357-904b9bb8a0f7
* Proposition de correction pour le bug #1173 (ou du moins pour unGravatar herbelin2007-04-13
| | | | | | | | | | exemple de divergence soumis par Andrew Appel) [on renonce à normaliser pour trouver l'ensemble minimal de variables liées dans le 2e membre d'une égalité dépendante] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9765 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #1477 sur ordre des variables partagées par les or-patterns.Gravatar herbelin2007-04-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9764 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test non régression bug #1491Gravatar herbelin2007-04-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9763 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #1491Gravatar herbelin2007-04-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9761 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 17:57:26 +0000