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
transform the toolbar icons for display of information into a Display menu with shortcuts
jnarboux
More... about 16 years ago
debug subst_command_placeholder : replace %s and not only %
jnarboux
More... about 16 years ago
Réorganisation des points d'appui du undo de CoqIDE (type reset_info).
herbelin
More... about 16 years ago
Encore un bug de undo
herbelin
More... about 16 years ago
Résolution bug #1850 sur notations avec niveaux inconnus de camlp4. Petit nettoyage en passant.
herbelin
More... about 16 years ago
Fix bashism in doc generation.
Stéphane Glondu
as glondu
More... about 16 years ago
Bug undo CoqIDE sur End
herbelin
More... about 16 years ago
the -g option is not recongnized in ocaml < 3.10.0
jforest
More... about 16 years ago
- Nouvelle option "Set Printing Existential Instances" pour forcer 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 !).
herbelin
More... about 16 years ago
- Prise en compte des frozen state de Coq autant que possible pour 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.
herbelin
More... about 16 years ago
Ajout de la possibilité d'utiliser fix/cofix dans les notations.
herbelin
More... about 16 years ago
doc of coqchk + improved module cache and computation of module sets
barras
More... about 16 years ago
Cyclic31 : replace the ugly time-consuming brute-force proof by a reasonable one. Conversion to lists of digits is really the Right Way (TM). Maybe other parts can also benefit from this idea. To be continued...
letouzey
More... about 16 years ago
- Fix bug #1858, Hint Unfold calling the wrong locate function. - 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.
msozeau
More... about 16 years ago
Nouvelle doc pour les modules.
soubiran
More... about 16 years ago
(Not completely finished) proofs that int31 integers fulfill the CyclicAxioms specs
letouzey
More... about 16 years ago
Strategy commands are now exported
barras
More... about 16 years ago
fixed dependency problems with the checker
barras
More... about 16 years ago
writing a match on a digit via syntax "if ... then ... else" is not a good idea :-( (some bad interaction with Arnaud's framework ??)
letouzey
More... about 16 years ago
Proposition for a almost-bitsize-independent Int31.v (joint work with J. Vouillon) As said at the beginning of the file:
letouzey
More... about 16 years ago
QRewrite is now obsolete. It was containing manual ltac stuff for helping rewriting under Quantifiers and binders, but Matthieu's setoid rewrite now has the same kind of capabilities by default.
letouzey
More... about 16 years ago
Should fix the dependancy issue mentioned by J.Forest about NMake: .v.d are created exactly for all $(VFILES), which was only a "find -name .v", so $(GENVFILES) should be added to $(VFILES)
letouzey
More... about 16 years ago
switch theories/Numbers from Set to Type (both the abstract and the bignum part).
letouzey
More... about 16 years ago
improved coqchk targets
barras
More... about 16 years ago
added coqchk to the main Makefile and a make variable VALIDATE to check the vo files of the theories
barras
More... about 16 years ago
refined the conversion oracle
barras
More... about 16 years ago
refined the conversion oracle
barras
More... about 16 years ago
Désactivation affichage image coqide en attendant un barcelos
herbelin
More... about 16 years ago
Correction bugs ide undo et highlight (suite à typos)
herbelin
More... about 16 years ago
Correction d'un bug de l'unification pattern qui oubliait d'expanser les alias avant de déclarer qu'une evar n'était appliquée qu'à des variables.
herbelin
More... about 16 years ago