Open Hub
Black Duck Open Hub

 Settings |  Report Duplicate

0
I Use This!
Inactive

Commits : Listings

Analyzed 2 days ago. based on code collected 2 days ago.
May 31, 2023 — May 31, 2024
Commit Message Contributor Files Modified Lines Added Lines Removed Code Location Date
- On adopte finalement la méthode de Pierre Courtieu pour le undo de proof general (caractérisation des undos comme triplet d'un nombre de Undo, n'un nombre de Abort et d'un Reset vers un état/id). C'est plus simple et cela permet en plus d'avoir des buts imbriqués. Au passage, "goto point" se comporte comme une suite de "one step back". - Quelques bricoles sur la fenêtre préférences de Shortcuts. - Quelques réorganisations autour du menu Display.
herbelin
More... almost 16 years ago
Quelques infos pour la portabilité 8.1 --> 8.2
notin
More... almost 16 years ago
One (last?) more update of CHANGES.
letouzey
More... almost 16 years ago
changed w_coerce_to_type to consider remaining unif problems (Hugo\'s patch)
barras
More... almost 16 years ago
Fix typos
lmamane
More... almost 16 years ago
Renommage id dans le test Nametab (suite ajout d'une constante de ce nom dans l'état initial)
herbelin
More... almost 16 years ago
Correctly catch UnresolvableConstraint exception which is now located. Fixes Sophia/Float.
msozeau
More... almost 16 years ago
more updates of CHANGES
letouzey
More... almost 16 years ago
Fixes incorrect handling of existing existentials variables in typeclass code.
msozeau
More... almost 16 years ago
Fix setoid_rewrite documentation examples. Debug handling of identifiers in coqdoc (should work with modules and sections) and add missing macros. Move theories/Program to THEORIESVO to put the files in the standard library documentation.
msozeau
More... almost 16 years ago
improve name, size and position of detached windows
jnarboux
More... almost 16 years ago
Some updates of CHANGES (to be continued...)
letouzey
More... almost 16 years ago
try to reduce the size of the queries pane
jnarboux
More... almost 16 years ago
Temporarily disabling automatic test for bug 1338.v
notin
More... almost 16 years ago
In abstract parts of theories/Numbers, plus/times becomes add/mul, for increased consistency with bignums parts
letouzey
More... about 16 years ago
In abstract parts of theories/Numbers, plus/times becomes add/mul, for increased consistency with bignums parts
letouzey
More... about 16 years ago
Minor bug correction in recdef
jforest
More... about 16 years ago
Petites corrections diverses : - bug d'installation (coq_config.cmo était installé une 2ème fois au lieu d'installer coq_config.cmx) - suite nettoyage configure, option reals - ajout d'une option "only parsing" oubliée dans Peano.v
herbelin
More... about 16 years ago
newton iteration for sqrt31
thery
More... about 16 years ago
Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided in a Coq meeting some time ago. NB: this syntax is an alias for (x,(y,(z,t)))
letouzey
More... about 16 years ago
remove additional occurrences of +/- forgotten in commit 11030
letouzey
More... about 16 years ago
On cesse de demander une valeur pour l'option reals si l'utilisateur n'en donne pas (ça paraît plus simple vu que le temps de compil de reals est devenu mineur, et on fait comme pour fsets qui par défaut est compilé).
herbelin
More... about 16 years ago
Bactrack sur +, - dans rewrite qui, redondants avec ->, <-, n'en sont qu'à peine plus courts.
herbelin
More... about 16 years ago
Quelques amendements liées à la compilation des packages. - typo du configure; - warnings variables non utilisées dans ide/utils; - suppression des variables vides COQINSTALLPREFIX et OLDROOT parce que l'option -e que l'on aurait pu en principe utiliser pour les surcharger ne fonctionne pas lorsqu'il y a plusieurs niveaux d'imbrication de makefiles (comme c'est le cas quand on vient du makefile servant à faire les packages qui appelle le makefile principal qui appelle les makefile.stage); - utilisation de ALLVO plutôt qu'un find pour trouver les .v sur lesquels appliquer coqdep (permet d'éviter des warning sur les fichiers de test, non prévus pour faire partie de la biblio standard); - utilisation de -custom sur les bytecode qui ne l'étaient pas encore (coqchk et coqmktop) pour être indépendant de ocamlrun à l'installation.
herbelin
More... about 16 years ago
BigQ: starting to create and use an interface QSig
letouzey
More... about 16 years ago
Enhance the BigN and BigZ infrastructure:
letouzey
More... about 16 years ago
Fix last commit about revision: I'm unsure about the role of "set -e", but it probably works only if placed in front of the shell line
letouzey
More... about 16 years ago
Attempt to avoid killing+recreating the file revision with same content. This should prevent some useless coqtop+theories recompilation
letouzey
More... about 16 years ago
Improvements on coqdoc by adding more information into .glob files, about definitions and type of references. - Add missing location information on fixpoints/cofixpoint in topconstr and syntactic definitions in vernacentries for correct dumping. - Dump definition information in vernacentries: defs, constructors, projections etc... - Modify coqdoc/index.mll to use this information instead of trying to scan the file. - Use the type information in latex output, update coqdoc.sty accordingly. - Use the hyperref package to do crossrefs between definition and references to coq objects in latex.
msozeau
More... about 16 years ago
Improve the dependent induction tactic to automatically find the generalized hypotheses. Also move part of the tactic to ML and improve the generated proof term in case of non-dependent induction.
msozeau
More... about 16 years ago