aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2007-10-12Maj du lien vers coq-bugs dans Coqidenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10219 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-11Allow a few build system optimisations/corner-cuttinglmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10218 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-11Bug variable CAMLP4 qui ne doit pas contenir un chemin mais le type de ↵herbelin
preprocesseur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10214 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-10Allowing setoid_reflexivity_in to work on quantified hypothesis (bug #1710) letouzey
(patch by J. Forest) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10212 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-10Mise à jour des notes d'installation pour Coqidenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10211 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-10Ajout d'une note sur Ocaml 3.10.0 et camlp5notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10210 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-09Extraction now checks that the required libraries are indeed loaded (bug #1144)letouzey
If a library is Require'd from inside an "opaque" Module (e.g. a module with an interface given by a ":"), then the required library is not loaded anymore after closing this module. We add an error in this situation, asking the user to manually do a Require before performing the Extraction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10208 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-09forbid extraction under a module typeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10206 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-09Extract Inline/Inductive/Constant can now be used from inside a moduleletouzey
It even seems to work from inside a functor. Fix old bug #472. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10204 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-09Verification ocaml >= 3.09.3 pour coq natif sous MacOS X Pentiumherbelin
+ uniformisations des messages utilisateurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10203 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-09Oubli de GTK pour Windows + typonotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10201 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-09Mise à jour de README.winnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10200 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-09Amélioration de l'appel aux outils externes via Coqidenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10199 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-08documentation of commit 10188letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10198 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-08Calcul des dependances sous Windowsnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10196 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-08Better use of tables for storing results of extract_ind (bug #1709)letouzey
It is critical to avoid duplicated calls to extract_ind (see e.g. example in #1709). But the same kernel_name can lead to different inductive bodies, due to module substitutions. So we used to factorize only "visible" kn, that were not subject to change under substitution. As shown by P. Cregut in #1709, this is not enough. New approach is now to store also Coq inductive data (mib). If the recorded mib matches the current one, we trust the recorded result, otherwise we start a fresh computation of extract_ind. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10194 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-08add $COQTOP to the search path of ocamldebugletouzey
in a debug session with ocamldebug 3.10, it was looking for file like contrib/foo/bar.ml and not just bar.ml in directories like contrib/foo, hence failing to find such a file. A quick fix is to add $COQTOP itself to the search path. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10193 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 20:56:07 +0000