aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2007-10-30temporary workaround for bug #1738letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10278 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-30A useless Add Morphism: since Subset is a Setoid Relation, it is alsoletouzey
automatically a Morphism about itself (avoid a warning about redeclared Setoids). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10277 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-30bug in safe_typing: univ constraints generated by section variables were not ↵barras
stored in modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10275 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-30Changement esthétique de la preuve de mult_is_onenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10274 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-30Ajout de lemmes d'inversion pour mult (sur le modèle de plus_is_O et ↵notin
plus_is_one) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10273 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-30Cleaning code and comment.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10272 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-29Revision of the FSetWeak Interface, so that it becomes a precise letouzey
subtype of the FSet Interface (and idem for FMapWeak / FMap). 1) No eq_dec is officially required in FSetWeakInterface.S.E (EqualityType instead of DecidableType). But of course, implementations still needs this eq_dec. 2) elements_3 differs in FSet and FSetWeak (sort vs. nodup). In FSetWeak we rename it into elements_3w, whereas in FSet we artificially add elements_3w along to the original elements_3. Initial steps toward factorization of FSetFacts and FSetWeakFacts, and so on... Even if it's not required, FSetWeakList provides a eq_dec on sets, allowing weak sets of weak sets. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10271 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-29Amélioration du message d'erreur dans end_module, end_module_type et ↵notin
close_section. On affiche maintenant le nom du dernier module/section ouvert git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10269 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-29MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10268 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-27Réparation d'une inefficacité bêtement introduite dans la révisionherbelin
10222: n'évaluer les std_ppcmds que si vraiment ils sont utilisés (en particulier, les [< ... >] sont paresseux comme on l'attend mais pas les ++). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10267 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-25small fix of commit 10188: a string given via Extract Inductive can be emptyletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10266 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-25Adding BigQ and proofsthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10265 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-25Added NIso.v to Makefile.common. Changed Examples.v in contrib/micromega to ↵emakarov
use NRing instead of Ring_polynom. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10264 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-24Quelques exemples à méditer sur le polymorphisme d'universe des inductifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10263 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-24Fix define body bug fixmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10262 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-24Fix define body bugmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10261 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-24Addition of more general tactics for equality. Functional extensionality and ↵msozeau
eta expansion axioms for dependent functions. Cleanup in Utils. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10260 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-24Bugfix in abstract_generalizemsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10259 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-24Doc updatemsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10258 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-24Fix some bugs, add possibility of automatically solving a proof statement's ↵msozeau
obligations and start the proof afterwards. Changes the architecture of subtac_obligations a bit. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10257 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-23Enlevé les trucs commités au mauvais endroitaspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10252 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-23Quelques structures de donnée plus les modules principaux (et aspiwack
parfaitement en cours) de la nouvelle machinerie de preuves. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10251 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-23Added "is_empty" to gmap.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10250 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-23Ajout de mots clés pour Coqdoc (bug #1732)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10248 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-23Added Numbers/Natural/Abstract/NIso.v that proves that any two models of ↵emakarov
natural numbers are isomorphic. Added NatScope and IntScope for abstract developments. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10247 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-22Corrections des bugs #1730 et #1731notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10246 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-21An error message instead of an empty extraction when the monolithic letouzey
extraction is given the name of a .v Module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10245 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-21Avoid the auto-inlining of small fixpoints like List.map.letouzey
A better eta-reduction allows to detect that List.map is indeed a fixpoint. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10244 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-21Cleanup attempt of Hints in *Interface.v files.letouzey
See recent discussion in coq-club. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10243 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-19Adding Zdiv_mod_unique, Zdiv_opp_opp, Zdiv_mult_cancel, and Z_div_leroconnor
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10242 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-18Intallation des .cma/.cmxanotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10241 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-18Changed RingMicromega to use NRing instead of Ring_polynom. NRing is a ↵emakarov
version of Ring_polynom written by Frederic Besson that uses binary trees instead of lists for environments. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10240 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-18Copie de PreOmega.vo dans le répertoire d'installation de Coqnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10239 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-18Copie des .cma et des .cmxa, et de grammar.cma dans le répertoire de Coq ↵notin
(pour faciliter la compilation des tactiques ml par les utilisateurs) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10238 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-18Typo dans Makefile.commonnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10237 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-18Report de la révision #10197 (adaptation à Lablgtk 2.10.0)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10236 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-18Uniformisation de l'option -where de coqc avec celle de coqtopnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10235 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-18added generation from trivial patterns for congruencecorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10234 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-17Repair Haskell/Scheme extraction in the new extraction backend design: letouzey
Unlike prlist_xxxx and prvect, the function prlist is acting lazily, which is bad for extraction (synchronization with tables). We add and use a prlist_strict function. Additionaly: - cleanup of the preamble printing - no need for 2-pass printing (/dev/null trick) when the language isn't ocaml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10233 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-17Major reorganisation of the extraction "backend".letouzey
Initial Idea: getting rid of nasty renaming issues in modules, in particular bugs #820 (part d) #1340 #1526 #1654 Final effect: lots of changes, simplifications, cleanups, unrelated fixes and ehancements, and also probably some regressions (time will tell). A few details: * no more experimental "Toplevel" language. * no more functors Make in Ocaml/Haskell/Scheme. The spirit of these functors and Mlpp_params was already not followed much, and this framework was more a nuisance that anything else. * instead, some records language_descr regrouping the specific features of the different output languages. * Common now comes before Ocaml/Haskell/Scheme, these ones are now independant from each others. print_structure_to_file is now in Extract_env. * A nice detail: no more duplications of warnings concerning axioms. * In modular extraction, the clashes due to the opened modules are now computed once and for all thanks to record_contents_fstlev, instead of re-asking Coq each time about these opened modules and using Extraction.constant_kind * some utilities about modules_path added and/or moved from Modutil to Table. * using a .v file as a module, e.g. in a functor application should now works in modular extraction. Now concerning renaming issues themselves: * printing is done twice, the first time toward /dev/null, in order to encounter the naming issues unsolvable by a simple qualification. On the second run, we create artificial modules Coq__123 for allowing qualification of these hidden objects. * names are now fully separated into their syntaxic categories: terms/types/constructors/modules * Only one last unsupported situation (but at least detected and signaled by an error): an object M.t from an external file-module M.v can't be printed when a local module M is in the way. This situation is really unlikely (in Coq you must use _long_ file-module name, e.g. Init.Datatypes.nat). It could be solved by inserting "module Coq_123 = M" at the beginning of the file, but then the signature of Coq_123 (that is, the one of M) should be written explicitely in the .mli, which is _really_ not nice. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10232 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-17Prise en compte des .glob par coq_makefilenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10231 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-16add visibility of extraction messages in coqideletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10230 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-16Correction d'un bug de l'appel à make via Coqidenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10229 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-16Fixed congruence instance generator + changed default depth to 1000corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10227 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-16Added transitivity and irreflexivity of <, as well as < -elimination for ↵emakarov
binary positive numbers. Added directory contribs/micromega with the generalization of Frédéric Besson's micromega tactic for an arbitrary ordered ring. So far no tactic has been defined. One has to apply the theorems and find the certificate, which is necessary to solve inequations, manually. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10226 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-16 Added the doc for the new Scheme Equality commandvsiles
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10225 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-16Vérification que "rewrite in" se comporte comme "rewrite" et échoueherbelin
sans bêta-normaliser face à un bêta-rédex dont l'argument ne correspond pas à ce qui est à réécrire. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10224 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-15build system: When using GOTO_STAGE, always go into that stage, even when ↵lmamane
target already exists git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10223 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-12- Préservation des appels récursifs de tête dans ltac (réponse au "wish"herbelin
implicite du rapport de bug #468); utilisation pour cela d'un mécanisme différent de localisation des échecs Ltac (mécanisme probablement à affiner). - Factorisation au passage des appels au débuggeur Ltac. - Trivialités en passant dans clenv.ml. - Tentative de documentation de l'infâme Reductionops.instance et essai de déplacement plus amont du test "s = []". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10222 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-12Uniformisation du comportement de rewrite et rewrite in : quand leherbelin
filtrage d'ordre 2 échoue à trouver un prédicat de réécriture qui n'est pas une K-abstraction, les deux rewrite essaie alors le filtrage d'ordre 1. Ce n'est pas le plus élégant mais c'est la solution uniforme permettant d'être conservatif. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10221 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-09 09:32:09 +0000