aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* Report 10087, 10089, 10090 de 8.1 vers trunk (compatibilité camlp5 et ↵Gravatar herbelin2007-08-24
| | | | | | -rectypes) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10091 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation plus précise de la contrainte de type pour interpréter lesGravatar herbelin2007-08-24
| | | | | | | | | | | points-fixes: on applique maintenant cette contrainte avant de généraliser corps et types vis à vis du context (utile notamment en présence de let-in dont on ne sait pas sinon s'ils font partie de la contrainte de type ou du contexte de typage). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10088 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1634 + ajout de bugs dans la test-suiteGravatar notin2007-08-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10085 85f007b7-540e-0410-9357-904b9bb8a0f7
* Save IS NOT the same Defined ....Gravatar msozeau2007-08-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10084 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Correction bug dans syntaxe des match (liste de motifs vide était acceptée)Gravatar herbelin2007-08-22
| | | | | | | - Des open en plus dans le débogueur-traceur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10083 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un warning losrqu'un nom de bibliothèque est ambigüGravatar notin2007-08-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10082 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification de l'initialisation des chemins de la librairie standardGravatar notin2007-08-20
| | | | | | | | | pour imposer un ordre précis des répertoires (résout en partie le problème entre Init.Wf et Program.Wf.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10081 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo in INSTALL instructionsGravatar lmamane2007-08-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10080 85f007b7-540e-0410-9357-904b9bb8a0f7
* Erreur de copier/coller dans la section GuardedGravatar notin2007-08-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10079 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1322Gravatar notin2007-08-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10077 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1680: ajout d'un champ avoid_ids dans interp_sign;Gravatar notin2007-08-16
| | | | | | | | | modification de interp_ltac_reference pour passer les ids utilisées dans le contexte d'appel d'une tactique. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10076 85f007b7-540e-0410-9357-904b9bb8a0f7
* An update on axiomatic number classes.Gravatar emakarov2007-08-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10075 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction (partielle) bug #1052 (coqdoc supprime les fins de ligne après ↵Gravatar notin2007-08-13
| | | | | | un commentaire) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10074 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1635Gravatar notin2007-08-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10073 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un exemple d'inversion des dépendances dans le prédicat commeGravatar herbelin2007-08-10
| | | | | | | implicitement suggéré par le rapport de bug #1671 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10072 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Correction d'un bug de de Bruijn dans abstract_predicate (lié auGravatar herbelin2007-08-10
| | | | | | | | | | | | rapport de bug #1671 - mais ne résoud pas le #1671 dans le propos peut être vu comme le souhait de voir traité le cas simple du problème généralement indécidable d'inversion des contraintes des types inductifs) - Petite amélioration dans le nommage des variables dans expand_arg git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10070 85f007b7-540e-0410-9357-904b9bb8a0f7
* TypoGravatar notin2007-08-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10069 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification de la test suite pour intégrer des tests spécifiques auxGravatar notin2007-08-10
| | | | | | | | bugs soumis sur Coq-bugs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10068 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification de control_only_guard, qui utilise maintenantGravatar notin2007-08-09
| | | | | | | | | | | | iter_constr_with_full_binders + documentation de Guarded. --Cette ligne, et les suivantes ci-dessous, seront ignorées-- M trunk/doc/refman/RefMan-pro.tex M trunk/pretyping/inductiveops.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10065 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix dependency bugs due to Program modules renamings.Gravatar msozeau2007-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10064 85f007b7-540e-0410-9357-904b9bb8a0f7
* Several simple new theorems in ZArith/BinInt.v and ZArith/Zbool.vGravatar emakarov2007-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10063 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a test case for the new "dependent" induction tactics.Gravatar msozeau2007-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10062 85f007b7-540e-0410-9357-904b9bb8a0f7
* A better Program documentation. Include it in the generated stdlib doc.Gravatar msozeau2007-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10061 85f007b7-540e-0410-9357-904b9bb8a0f7
* Move Program tactics into a proper theories/ directory as they are general ↵Gravatar msozeau2007-08-07
| | | | | | purpose and can be used directly be the user. Document them. Change Prelude to disambiguate an import of a Tactics module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10060 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a new tactic to generalize an instantiated inductive predicate adding ↵Gravatar msozeau2007-08-07
| | | | | | equalities. Useful to do so-called "ford" induction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10059 85f007b7-540e-0410-9357-904b9bb8a0f7
* Build system: _really_ don't recurse into VCS metadata for file listsGravatar lmamane2007-08-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10058 85f007b7-540e-0410-9357-904b9bb8a0f7
* Build system:Gravatar lmamane2007-08-07
| | | | | | | | - BSD compatibility: do not use -printf action of find (2nd round) - don't recurse into VCS metadata for file lists git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10057 85f007b7-540e-0410-9357-904b9bb8a0f7
* Build system: BSD compatibility: do not use -printf action of findGravatar lmamane2007-08-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10056 85f007b7-540e-0410-9357-904b9bb8a0f7
* mul and sqrtGravatar thery2007-07-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10055 85f007b7-540e-0410-9357-904b9bb8a0f7
* Corrected the reference to glob.dump, which is used to create ↵Gravatar emakarov2007-07-26
| | | | | | stdlib/index-body.html. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10051 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add glob.dump to Makefile the recommended way and document theGravatar lmamane2007-07-25
| | | | | | | recommended way more explicitly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10050 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modifications de la construction de la documentation de la librairieGravatar notin2007-07-25
| | | | | | | | | | | | | standard: - ajout d'une entrée dans le Makefile principal pour le fichier de globalisations glob.dump - modifications de doc/Makefile et de l'index html pour gérer les nouveaux fichiers de la librairie standard (en part. ceux dans Ints) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10049 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pattern matching sur BigN.N13 manquant dans les fonctions do_norm_n etGravatar notin2007-07-25
| | | | | | | | do_norm. Corrigé par analogie avec N11, N12, ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10048 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed bug 1448 and 1674Gravatar barras2007-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10046 85f007b7-540e-0410-9357-904b9bb8a0f7
* proof of compare addedGravatar thery2007-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10045 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed bug 1675: computing carrier from the relation type was not rightGravatar barras2007-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10043 85f007b7-540e-0410-9357-904b9bb8a0f7
* Declarative language: fixed the generation of fixpoints for induction proofs.Gravatar corbinea2007-07-24
| | | | | | | | Cleaner code: the guardedness bug is now corrected. Added "trivial" to the automation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10042 85f007b7-540e-0410-9357-904b9bb8a0f7
* An update on axiomatization of numbers.Gravatar emakarov2007-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10041 85f007b7-540e-0410-9357-904b9bb8a0f7
* removed thesisGravatar barras2007-07-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10040 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation of Program and its tactics, fix enormous interaction bug due ↵Gravatar msozeau2007-07-19
| | | | | | to bad cache handling. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10032 85f007b7-540e-0410-9357-904b9bb8a0f7
* some more svn:ignore propertiesGravatar letouzey2007-07-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10029 85f007b7-540e-0410-9357-904b9bb8a0f7
* A generic preprocessing tactic zify for (r)omegaGravatar letouzey2007-07-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ------------------------------------------------ See file PreOmega for more details and/or test-suite/succes/*Omega*.v The zify tactic performs a Z-ification of your current goal, transforming parts of type nat, N, positive, taking advantage of many equivalences of operations, and of the positivity implied by these types. Integration with omega and romega: (r)omega : the earlier tactics, 100% compatible (r)omega with * : full zify applied before the (r)omega run (r)omega with <types>, where <types> is a sub-list of {nat,N,positive,Z}, applies only specific parts of zify (btw "with Z" means take advantage of Zmax, Zmin, Zabs and Zsgn). As a particular consequence, "romega with nat" should now be a close-to-perfect replacement for omega. Slightly more powerful, since (forall x:nat, x*x>=0) is provable and also slightly less powerful: if False is somewhere in the hypothesis, it doesn't use it. For the moment zify is done in a direct way in Ltac, using rewrite when necessary, but crucial chains of rewrite may be made reflexive some day. Even though zify is designed to help (r)omega, I think it might be of interest for other tactics (micromega ?). Feel free to complete zify if your favorite operation / type isn't handled yet. Side-effects: - additional results for ZArith, NArith, etc... - definition of Ple, Plt, Pgt, Pge and notations for them in positive_scope - romega now start by doing "intros". Since the conclusion will be negated, and this operation will be justified by means of decidability, it helps to have as little as possible in the conclusion. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10028 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: slightly cleaner version of r10026Gravatar lmamane2007-07-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10027 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: don't mention bin/coqtop.byte twice to make when BEST=byte, it ↵Gravatar lmamane2007-07-18
| | | | | | complains. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10026 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleanly refuse to operate in the presence of unsaved changes in emacsGravatar lmamane2007-07-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10025 85f007b7-540e-0410-9357-904b9bb8a0f7
* Affichage de "thesis" seulement en mode déclaratifGravatar herbelin2007-07-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10024 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oups... Use shell-variable syntax in shell commands.Gravatar lmamane2007-07-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10023 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: Revert r10015, which was based on a misunderstandingGravatar lmamane2007-07-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10022 85f007b7-540e-0410-9357-904b9bb8a0f7
* Raffinement de interp_ident pour que l'ident interprété soit au choixGravatar herbelin2007-07-18
| | | | | | | | frais (par exemple pour "intro") ou pas forcément (par exemple pour "fresh") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10021 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: needs GNU Make 3.81Gravatar lmamane2007-07-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10020 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-05 03:40:52 +0000