aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2008-05-28CyclicAxioms: after discussion with Laurent, znz_WW and variants areletouzey
transformed into generic functions, and aren't anymore fields of records znz_op/znz_spec. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11012 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-28replace the query window of coqide by a pane in main window as suggested by hugojnarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11011 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-28introduced Termops.eq_constr (and constr_cmp) that compares terms up to ↵barras
alpha AND universe erasure git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11010 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-28add option to change modifiers of display menujnarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11009 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-28update gtk requirementsjnarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11008 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-28Réorganisation fenêtre d'accueil CoqIDE et About; nouvelle image deherbelin
coq (mais ça ne rend pas très bien -- faudrait centrer l'image) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11007 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-28add support for pdf in coqdoc, add export to pdf in coqide, port open and ↵jnarboux
save as dialogs of coqide to a not deprecated widget, add filtering of *.v files in these dialogs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11006 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-28debug : case where length of s is < 2...jnarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11005 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-28- Correction bug highlighting "Module" dans Coqideherbelin
- Divers code mort (evarutil.ml, Bvector.v) - MAJ perf-analysis git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11004 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-28Cyclic31: proofs for addmuldiv31, tail031 and head031. Only two Admitted left !letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11003 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-27Cyclic31: proof of auxiliary function iter_int31 + (failed) attempt at ↵letouzey
proving addmuldiv31 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11002 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-27Correction du problème de complexité de Print Assumptions :aspiwack
- Suite à une modification faite maladroitement, on ne se contentait pas de comparer le nom de la supposition quand on l'insérait dans l'ensemble des suppositions utilisées, mais aussi son type, ce qui était inutilement long (mais pas le facteur principal) - L'environnement était parcouru deux fois pour chaque variable de section. Ce n'était pas très grave vu qu'en général on a assez peu de variables de sections sous la main. Mais ça restait inutile. - Les noms qui ont déjà étés explorés sont maintenant memoizés, ce qui gagne dans le cas les pires (comme les théorèmes sur les réels typiquement) une exponentiel dans le temps de recherche (si on visualise l'espace de recherche comme un DAG, l'ancienne procédure le parcourais comme si il était un arbre, ce qui a une complexité exponentielle en la taille du DAG). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11001 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-27add install instruction for mandrivajnarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11000 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-27Cyclic31: migrate auxiliary lemmas to their legitimate filesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10999 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-27update changes related to coqidejnarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10998 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-23 22:31:04 +0000