| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
| |
typeclass code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11047 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
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.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11046 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11044 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11043 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11042 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11041 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
for increased consistency with bignums parts
(commit part II: names of files + additional translation minus --> sub)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11040 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
for increased consistency with bignums parts
(commit part I: content of files)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11039 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11036 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
- 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
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11035 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11034 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
a Coq meeting some time ago. NB: this syntax is an alias for (x,(y,(z,t)))
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11033 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11032 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
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é).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11031 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
peine plus courts.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11030 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- 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.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11029 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11028 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Isolate and put forward the interfaces NSig and ZSig that describe
what should contain structures of natural numbers and integers (specs
are done by translation to ZArith).
* Functors NSigNAxioms and ZSigZAxioms proving that these NSig and
ZSig implements the fully-abstract NAxioms and ZAxioms module types.
* BigN and BigZ now contains more notations, plus an export of all
abstract results proved by Evgeny instantiated thanks to NSigNAxioms
and ZSigZAxioms. In addition, BigN and BigZ are declared as
(semi/full)-rings.
* as a consequence, some incompatibities have to be fixed in BigQ:
- take care of some name masking (via Import, Open Scope ...)
- some additionnal constants like BigN.lt to deal with
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11027 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
but it probably works only if placed in front of the shell line
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11026 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
This should prevent some useless coqtop+theories recompilation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11025 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
Next step is to test and debug it on bigger developments.
On the side:
- Fix Program Let which was adding a Global definition.
- Correct implicits for well-founded Program Fixpoints.
- Add new [Method] declaration kind.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11024 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
generalized hypotheses. Also move part of the tactic to ML and
improve the generated proof term in case of non-dependent induction.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11023 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
n'étaient pas gérés, merci à Julien).
- Correction pb blocage CoqIDE quand le browser n'est pas déja lancé
(utilisation pour cela de Sys.command au lieu de Unix.open_process_full).
- MAJ CHANGES et COMPATIBILITY.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11022 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
should not loop)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11021 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11020 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11019 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11018 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11017 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11016 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
Assia et Benjamin W. de telle sorte qu'ils respectent le critère de
décroissance structurelle lorsqu'utilisés dans un point-fixe.
- Ajout des noms "standard" des lemmes de Peano et correction d'un nom de
BinInt.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11015 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
impossibles dans un filtrage dépendant.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11014 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
now dumb wrappers around Zsqrt_plain. Wanted (dead or alive): better
implemntations _and_ their proofs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11013 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11011 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
alpha AND universe erasure
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11010 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11009 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11008 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
| |
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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11005 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
- 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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11003 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
proving addmuldiv31
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11002 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- 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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11000 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10999 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10998 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10997 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10996 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10995 85f007b7-540e-0410-9357-904b9bb8a0f7
|