aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2008-06-09Fix a typoglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11081 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-09Documentation de "instantiate".glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11080 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-09Remplacement des echo -e par printf + bug sur les exécutables ocaml dans ↵notin
coq_makefile git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11079 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-09On prend des risques en tentant d'optimiser encore plus le undo en casherbelin
de preuves imbriquées. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11078 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-09- Documentation de admit et Print Assumptions.herbelin
- Relecture, mise à jour, correction d'erreurs et petite réorganisation du chapitre sur les commandes vernaculaires. - Correction bug #1865 (rafraichissement des univers algébriques). - Suppression de la dépendance du initial.coq en les noms longs des fichiers de façons à ce que les dépendances ne soient que purement logique. - Encore un (petit) bug undo ide. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11077 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-09more uniform name of app for windows classjnarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11076 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-09fix toggle item for show hide query panejnarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11075 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-09add confirmation dialog for printingjnarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11074 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-08- Patch sur "intros until 0"herbelin
- MAJ CHANGES et COMPATIBILITY - Réservation de || et && dans Notations.v - code mort et MAJ suite commit 11072 (tactics.ml et changes.txt) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11073 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-08- Extension de "generalize" en "generalize c as id at occs".herbelin
- Ajout clause "in" à "remember" (et passage du code en ML). - Ajout clause "in" à "induction"/"destruct" qui, en ce cas, ajoute aussi une égalité pour se souvenir du terme sur lequel l'induction ou l'analyse de cas s'applique. - Ajout "pose t as id" en standard (Matthieu: j'ai enlevé celui de Programs qui avait la sémantique de "pose proof" tandis que le nouveau a la même sémantique que "pose (id:=t)"). - Un peu de réorganisation, uniformisation de noms dans Arith, et ajout EqNat dans Arith. - Documentation tactiques et notations de tactiques. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11072 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-08enleve les majuscules dans Save All, comem suggéré pas Hugojnarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11071 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-08Second pass on typeclasses documentation, fix html rendering.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11070 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-07Correct handling of the environment in build_signature, and throwmsozeau
exception for dependent arrow types. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11069 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-07Change setoid_rewrite's matching semantics to continue matching insidemsozeau
matched occurences that are not selected. Permit to rewrite at 3 different places in (a + b) + (c + d) = 0 with a lemma ending in [_ + _]. Order is depth-first and left-to-right. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11068 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-07Fix library index template and associated script.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11067 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-07add tiny change to coqidejnarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11066 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-06Enhancements to coqdoc, better globalization of sections and modules.msozeau
Minor fix in Morphisms which prevented working with higher-order morphisms and PER relations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11065 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-06avoid duplicated creation of WFacts instancesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11064 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-06ajout d'un printer pour les contraintes d'univers + correction d'un bug sur ↵soubiran
les notations dans les alias de module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11063 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-062-3 petites modifs pour la compilation sous Windows...notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11062 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-06Copie des .cmi en plus des .cma et des .cmxanotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11060 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-06Correction terminologie et ajout plage unicode 1D400-1D7FF (mathematicalherbelin
alphanumerical symbols) suite à remarques de Arnaud. Correction bugs d'affichage de l'option -translate. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11059 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-06- On adopte finalement la méthode de Pierre Courtieu pour le undo deherbelin
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. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11058 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-05Quelques infos pour la portabilité 8.1 --> 8.2notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11057 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-05One (last?) more update of CHANGES.letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11056 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-05changed w_coerce_to_type to consider remaining unif problems (Hugo\'s patch)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11055 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-05Fix typoslmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11054 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-05Renommage id dans le test Nametab (suite ajout d'une constante de ceherbelin
nom dans l'état initial) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11053 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-05Correctly catch UnresolvableConstraint exception which is now located. msozeau
Fixes Sophia/Float. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11052 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-04more updates of CHANGESletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11049 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-03Fixes incorrect handling of existing existentials variables inmsozeau
typeclass code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11047 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-03Fix setoid_rewrite documentation examples.msozeau
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
2008-06-03improve name, size and position of detached windowsjnarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11044 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-03Some updates of CHANGES (to be continued...)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11043 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-03try to reduce the size of the queries panejnarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11042 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-03Temporarily disabling automatic test for bug 1338.vnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11041 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-03In abstract parts of theories/Numbers, plus/times becomes add/mul, letouzey
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
2008-06-02In abstract parts of theories/Numbers, plus/times becomes add/mul, letouzey
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
2008-06-02Minor bug correction in recdefjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11036 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-02Petites corrections diverses :herbelin
- 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
2008-06-02newton iteration for sqrt31thery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11034 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-01Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided inletouzey
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
2008-06-01remove additional occurrences of +/- forgotten in commit 11030letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11032 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-01On cesse de demander une valeur pour l'option reals si l'utilisateurherbelin
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
2008-06-01Bactrack sur +, - dans rewrite qui, redondants avec ->, <-, n'en sont qu'àherbelin
peine plus courts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11030 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-01Quelques amendements liées à la compilation des packages.herbelin
- 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
2008-06-01BigQ: starting to create and use an interface QSigletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11028 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-01Enhance the BigN and BigZ infrastructure: letouzey
* 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
2008-05-31Fix last commit about revision: I'm unsure about the role of "set -e", letouzey
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
2008-05-31Attempt to avoid killing+recreating the file revision with same content.letouzey
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-28 14:39:26 +0000