aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2008-05-27Cyclic31 : proof of the spec of gcd31letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10997 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-27revert toolbar to previous state: icons stylejnarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10996 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-26Int31 : gcd31 was wrongletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10995 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-26remove set printing ... and unset printing ... from template menu as they ↵jnarboux
are no useless in coqide git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10994 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-26Cyclic31: cleanup, 2 Admitted killed (6 remaining)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10993 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-26transform the toolbar icons for display of information into a Display menu ↵jnarboux
with shortcuts git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10992 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-26debug subst_command_placeholder : replace %s and not only %jnarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10991 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-26Réorganisation des points d'appui du undo de CoqIDE (type reset_info).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10990 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-26Encore un bug de undoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10989 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-26Résolution bug #1850 sur notations avec niveaux inconnus deherbelin
camlp4. Petit nettoyage en passant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10987 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-26Fix bashism in doc generation.glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10986 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-26Bug undo CoqIDE sur Endherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10985 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-26the -g option is not recongnized in ocaml < 3.10.0jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10984 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-25- Nouvelle option "Set Printing Existential Instances" pour forcerherbelin
l'affichage des instances des evars. - Nouveaux boutons "interrupteurs" pour activer/désactiver à volonté l'affichage des implicites, coercions, notations, etc dans CoqIDE (reste à trouver des icônes appropriées !). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10983 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-24- Prise en compte des frozen state de Coq autant que possible pourherbelin
améliorer l'efficacité du undo. Restent les Qed et les End dont le undo peut nécessiter de rejouer un segment arbitrairement complexe (pour le undo du Qed, il faudrait typiquement que Coq se souvienne de l'entrelacement de déclarations et de tactiques). - Code mort concernant les mots-clés dans coq.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10982 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-24Ajout de la possibilité d'utiliser fix/cofix dans les notations.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10981 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-23doc of coqchk + improved module cache and computation of module setsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10979 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-23Cyclic31 : replace the ugly time-consuming brute-force proof by a reasonable ↵letouzey
one. Conversion to lists of digits is really the Right Way (TM). Maybe other parts can also benefit from this idea. To be continued... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10978 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-23- Fix bug #1858, Hint Unfold calling the wrong locate function.msozeau
- Fix typeclass interface: instance_constructor now takes the instance constrs as argument to build and return the corresponding term and type. - Better typeclass error reporting when defining fixpoints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10975 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-23Nouvelle doc pour les modules.soubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10974 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-23(Not completely finished) proofs that int31 integers fulfill the ↵letouzey
CyclicAxioms specs Currently, 8 lemmas remains to tackle. One proof is done via a _very_ brute-force ugly approach. The all story for proving composition of phi and phi_inv (and the other way around) is surprisingly long and tricky. In both cases, comments are welcome, I may have missed an easier road (?) As a consequence of the above, we have a additional time-eager file in the stdlib (about a minute to compile here). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10973 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-22Strategy commands are now exportedbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10971 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-22fixed dependency problems with the checkerbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10970 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-22writing a match on a digit via syntax "if ... then ... else" is not a good ↵letouzey
idea :-( (some bad interaction with Arnaud's framework ??) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10969 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-22Proposition for a almost-bitsize-independent Int31.v (joint work with J. ↵letouzey
Vouillon) As said at the beginning of the file: This file contains basic definitions of a 31-bit integer arithmetic. In fact it is more general than that. The only reason for this use of 31 is the underlying mecanism for hardware-efficient computations by A. Spiwack. Apart from this, a switch to, say, 63-bit integers is now just a matter of replacing every occurences of 31 by 63. This is actually made possible by the use of dependently-typed n-ary constructions for the inductive type [int31], its constructor [I31] and any pattern matching on it. If you modify this file, please preserve this genericity. From the user point-of-view, almost nothing has changed: functions like On, In, shiftr, shiftl and a few others now have a syntactically-different definition, but thanks to Eval compute in their definition, this leads to the exact same coq objects as before. The only difference is "Check I31" that shows the compact n-ary version (nfun digits 31 int31) instead of (digits -> ... -> digits -> int31). But even "Print int31" shows the same answer as before (the above type of I31 is shown after expansion). Arnaud, could you check whether all this works fine with your retroknowledge ? Notice the new file NaryFunction that contain generic stuff about n-ary dependent functions. It should end some day in another place than theories/Numbers, but I cant figure where for now. This file is also quite skinny yet, but it's a start. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10967 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-22QRewrite is now obsolete. It was containing manual ltac stuffletouzey
for helping rewriting under Quantifiers and binders, but Matthieu's setoid rewrite now has the same kind of capabilities by default. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10966 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-22Should fix the dependancy issue mentioned by J.Forest about NMake: letouzey
.v.d are created exactly for all $(VFILES), which was only a "find -name .v", so $(GENVFILES) should be added to $(VFILES) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10965 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-22switch theories/Numbers from Set to Type (both the abstract and the bignum ↵letouzey
part). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10964 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-22improved coqchk targetsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10963 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-22added coqchk to the main Makefile and a make variable VALIDATE to check the ↵barras
vo files of the theories git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10962 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-21refined the conversion oraclebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10961 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-21refined the conversion oraclebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10960 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-21Désactivation affichage image coqide en attendant un barcelosherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10958 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-21Correction bugs ide undo et highlight (suite à typos)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10957 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-20Correction d'un bug de l'unification pattern qui oubliait d'expanserherbelin
les alias avant de déclarer qu'une evar n'était appliquée qu'à des variables. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10956 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-20Corrections d'erreurs rapportées par Frédéric Besson sur le précédentherbelin
commit de micromega + cache csdp complet. Quelques questions résiduelles : - où mettre l'interface entre coq et csdp (csdpcert) ? - micromega.ml est un fichier engendré par extraction : vaut-il le coup de compiler coq en deux fois, une 1e fois pour compiler et extraire micromega.ml, une seconde fois pour inclure micromega.ml ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10955 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-20added checker to svn:ignorebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10954 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-20also fixed conversion of the checkerbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10953 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-20Cleanup build_new, remove unneeded try-with and debug interaction ofmsozeau
on_morphisms and under_lambdas. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10952 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-20Léger backtrack sur commit coqide précédent (si la commande à annulerherbelin
à potentiellement modifié l'état, on ne peut se contenter d'un Abort : il faut revenir au dernier état connu). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10951 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-20Fixed coqide bug #1856 that was introduced in revision 10915.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10950 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-20Retrait d'un test commité par erreur en 10947herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10949 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-19MAJ créditsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10948 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-19Intégration de micromega ("omicron" pour fourier et sa variante sur Z,herbelin
"micromega" et "sos" pour les problèmes non linéaires sous-traités à csdp); mise en place d'un cache pour pouvoir rejouer les preuves sans avoir besoin de csdp (pour l'instant c'est du bricolage, faudra affiner cela). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10947 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-19Fix globalization bug in class_tactics and refactorize instancemsozeau
declaration code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10946 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-19Fix caml debug flags configuration, -g works with the native compiler onlymsozeau
since 3.10. Fix a bug in classes when the instance database is empty. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10945 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-19Minor improvement: group stuff about carry apart from stuff about zn2zletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10944 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-19Thanks to Matthieu's commit 10941, Ad-hoc tactics contained in QRewrite are ↵letouzey
no longer needed to compile theories/Numbers. QRewrite will probably be removed in a latter commit (need to check 2-3 things first with Matthieu and Evgeny) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10943 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-17ZModulo: Z viewed modulo 2^digits implements CyclicAxiomsletouzey
This isn't useful for BigN et BigZ, but it can't hurt; and moreover it's a simple way to understand CyclicAxioms. Next step: proving that Int31 is also an implementation of CyclicAxiom. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10942 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-17Fix a de Bruijn bug in setoid_rewrite when rewriting undermsozeau
a non-dependent product under a lambda. Now qiff can be replaced by a simple setoid_rewrite in NumPrelude. Change configure to not do stripping if compiling with -g... Add -g / CAMLDEBUG flags to the native compilation command too. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10941 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 02:55:56 +0000