aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* - Extracted from the tactic "now" an experimental tactic "easy" for smallGravatar herbelin2008-12-26
| | | | | | | | | | | | | | | | | automation. - Permitted to use evars in the intermediate steps of "apply in" (as expected in the test file apply.v). - Back on the systematic use of eq_rect (r11697) for implementing rewriting (some proofs, especially lemma DistOoVv in Lyon/RulerCompassGeometry/C14_Angle_Droit.v and tactic compute_vcg in Sophia-Antipolis/Semantics/example2.v are explicitly refering to the name of the lemmas used for rewriting). - Fixed at the same time a bug in get_sort_of (predicativity of Set was not taken into account). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11717 85f007b7-540e-0410-9357-904b9bb8a0f7
* 11715 continuedGravatar herbelin2008-12-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11716 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Optimized "auto decomp" which had a (presumably) exponential inGravatar herbelin2008-12-26
| | | | | | | | | the number of conjunctions to split. - A few cleaning and uniformisation in auto.ml. - Removal of v62 hints already in core. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11715 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Suppression date dans configure du trunkGravatar herbelin2008-12-26
| | | | | | | | | - Utilisation de get_version_date pour l'option -v (plutôt que la date non à jour du configure) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11714 85f007b7-540e-0410-9357-904b9bb8a0f7
* - coq_makefile: target install now respects the original tree structureGravatar herbelin2008-12-24
| | | | | | | | | | | | | of the archive to install in coq user-contrib installation directory. - Relaxed the validity check on identifiers from an error to a warning. - Added a filtering option to Print LoadPath. - Support for empty root in option -R. - Better handling of redundant paths in ml loadpath. - Makefile's: Added target initplugins and added initplugins to coqbinaries. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11713 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo in Makefile leading to empty quote_plugin.cmaGravatar letouzey2008-12-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11712 85f007b7-540e-0410-9357-904b9bb8a0f7
* FMap: fold_rec + more permissive transpose hyp + various cleanupGravatar letouzey2008-12-22
| | | | | | | The induction principles for fold are due to S. Lescuyer The better transpose hyp is a suggestion by P. Casteran git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11711 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage des variables Coq et amélioration de coqmktop. LesGravatar notin2008-12-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | principaux changements sont: - coqtop (et coqc) maintenant insensible aux variables d'environnement COQTOP, COQBIN et COQLIB; le chemin vers les librairies Coq peut être spécifié par l'option -coqlib - coqmktop prend 4 nouvelles options: -boot, -coqlib, -camlbin et -camlp4bin; en mode boot, coqmktop se réfère à Coq_config pour les chemins des exécutables OCaml; en dehors du mode boot, coqmktop cherche les exécutables OCaml dans PATH - installation des *.cmxs *.o et *.a en plus des *.cm[ioxa]; ceux-ci étant installé en copiant l'architecture des sources (ie lib.cmxa est installé dans COQLIB/lib/lib.cmxa) - coq_makefile prend maintenant 3 paramètres sous forme de variables d'environnement: COQBIN pour dire où trouver les exécutables Coq, CAMLBIN et CAMLP4BIN pour les exécutables OCaml et Camlp4/5; les chemins vers les librairies sont déduits en utilisant -where Le tout a testé avec Ssreflect (cf coq-contribs) en essayant de simuler les conditions de la vie réelle (Ocaml pas dans le PATH, installation binaire relocalisée, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11707 85f007b7-540e-0410-9357-904b9bb8a0f7
* Désactivation de dumpglob lors des appels a functional induction (erreurs ↵Gravatar notin2008-12-18
| | | | | | parasites du Lexer) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11706 85f007b7-540e-0410-9357-904b9bb8a0f7
* Maintenant on scan les .ml pour les .dot/.dep.ps (fait avec Matthias). Gravatar aspiwack2008-12-18
| | | | | | | | | | Rien de fait pour les .ml4 encore. De plus il y a une bizarrerie avec contradiction.ml qui plante sur coqdoc, ce n'est pas très grave, mais il faudra regarder un jour quand même... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11705 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout des fichiers de lib/ dans les dépendences générées par make Gravatar aspiwack2008-12-18
| | | | | | | | | | | coq.dep.ps et make coq.dot. Le résultat n'est pas très probant, car on continue à n'analyser que les .mli, on devrait sans doute analyser les .ml pour avoir les vrais dépendances de Coq. A suivre... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11704 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un bug causant un Not_found dans la contrib FSet.Gravatar soubiran2008-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11702 85f007b7-540e-0410-9357-904b9bb8a0f7
* FSets: integration of suggestions by P. Casteran and S. LescuyerGravatar letouzey2008-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11698 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixed cutrewrite bug #2021 introduced in commit 11662 (as a sideGravatar herbelin2008-12-18
| | | | | | | | | | | | | | | effect, old cut_replacing was betaiota-normalizing, new cut_replacing, from commit 11662, does not; turn betaiota-normalisation into a purer and simpler whd_beta of the abstracted rewriting predicate to the rewritten term). - Made "induction in" more flexible when induction is on a goal variable (accept occurrences -- even if theoretically unnecessary -- so as e.g. not to expand occurrences that would otherwise trigger reductions - see example in Peano.mult_succ_r). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11697 85f007b7-540e-0410-9357-904b9bb8a0f7
* Avoid printing that extraction has created file Foo when it's not the caseGravatar letouzey2008-12-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11695 85f007b7-540e-0410-9357-904b9bb8a0f7
* Better compatibility after commit 11693 by adding an alias ↵Gravatar letouzey2008-12-17
| | | | | | OrderedTypeFacts.eq_dec git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11694 85f007b7-540e-0410-9357-904b9bb8a0f7
* FSet/OrderedType now includes an eq_dec, and hence become an extension of ↵Gravatar letouzey2008-12-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | DecidableType After lots of hesitations, OrderedType now requires this "eq_dec" field, which is redundant (can be deduced from "compare"), but allows the subtyping relation DecidableType <= OrderedType, and hence WS <= S : ordered sets are now truly extensions of weak sets. Of course this change introduces a last-minute incompatibility, but: - There is a clear gain in term of functionnality / simplicity. - FSets 8.2 already needs some adaptations when compared with 8.1, so it's the right time to push such incompatible changes. - Transition shouldn't be too hard: the old OrderedType still exists under the name MiniOrderedType, and functor MOT_to_OT allows to convert from one to the other. Beware, for a FSetInterface.WS (resp. S) to be coercible to a DecidableType (resp. OrderedType), an eq_dec on sets is now required in these interfaces and in the implementations. In pratice, it is really easy to build from equal and equal_1 and equal_2. Some name changes : in FSetFacts, old WFacts now correspond to WFacts_fun, while WFacts now expects only one argument (WFacts M := WFacts_fun M.E M). Idem with WDecide, WProperties and WEqProperties. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11693 85f007b7-540e-0410-9357-904b9bb8a0f7
* Sequel of 11697: repair coqtop.byte when contribs are statically linked ↵Gravatar letouzey2008-12-17
| | | | | | (+minor improvements) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11692 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction Blacklist : a new command for avoiding conflicts with existing filesGravatar letouzey2008-12-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11690 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: also comply to Set Printing Width when producing external filesGravatar letouzey2008-12-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11688 85f007b7-540e-0410-9357-904b9bb8a0f7
* Take advantage of natdynlink when available: almost all contribs become ↵Gravatar letouzey2008-12-16
| | | | | | | | | | | | | | | | | | | | | | | | loadable plugins - Any contrib foo leads to contrib/foo/foo_plugin.cmxs (and .cma for bytecode). - Features that were available without any Require are now loaded systematically when launching coqtop (see Coqtop.load_initial_plugins): extraction, jprover, cc, ground, dp, recdef, xml - The other plugins are loaded when a corresponding Require is done: quote, ring, field, setoid_ring, omega, romega, micromega, fourier - I experienced a crash (segfault) while turning subtac into a plugin, so this one stays statically linked into coqtop for now - When the ocaml version doesn't support natdynlink, or if "-natdynlink no" is explicitely given to configure, coqtop is statically linked with all of the above code as usual. Some messages [Ignore ML file Foo_plugin] may appear. - How should coqdep handle a "Declare ML Module "foo"" if foo is an archive and not a ml file ? For now, we suppose that the foo.{cmxs,cma} are at the same location as the .v during the build, but can be moved later in any place of the ml loadpath. This is clearly an experimentation. Feedback most welcome... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11687 85f007b7-540e-0410-9357-904b9bb8a0f7
* Move FunctionalExtensionality to Logic/ (someone please check that theGravatar msozeau2008-12-16
| | | | | | | | | | doc is ok). Rework the .v files in Program accordingly, adding some documentation and proper headers. Integrate the development of an elimination principle for measured functions in Program/Wf by Eelis van der Weegen. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11686 85f007b7-540e-0410-9357-904b9bb8a0f7
* Finish fix for the treatment of [inverse] in [setoid_rewrite], making aGravatar msozeau2008-12-16
| | | | | | | | | | variant of the [unify] tactic that takes a hint db as argument and does unification modulo its [transparent_state]. Add test-file for bug #1939 and another [AdvancedTypeClasses.v] that mimicks [AdvancedCanonicalStructure.v]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11685 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix for syntax changes in test-suite scripts.Gravatar msozeau2008-12-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11684 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add some unicode symbols from japanese CJC (request by Y. Regis-Gianas)Gravatar letouzey2008-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11683 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix looping class resolution bug discovered by B. Aydemir and use theGravatar msozeau2008-12-14
| | | | | | | | right unification flags for exact hints in eauto (may break a lot of things by succeeding much more often). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11681 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes in the type classes documentation:Gravatar msozeau2008-12-14
| | | | | | | | | | | | - Document the new binders, now in sync with the implementation - Fix the examples - Redo the part about superclasses now that we got rid of "=>" - Add explanation of singleton "definitional" classes - Add info about the optional priority attribute of instances (thanks to M. Lasson for pointing it out). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11680 85f007b7-540e-0410-9357-904b9bb8a0f7
* Generalized binding syntax overhaul: only two new binders: `() and `{},Gravatar msozeau2008-12-14
| | | | | | | | | | | | | | | | | guessing the binding name by default and making all generalized variables implicit. At the same time, continue refactoring of Record/Class/Inductive etc.., getting rid of [VernacRecord] definitively. The AST is not completely satisfying, but leaning towards Record/Class as restrictions of inductive (Arnaud, anyone ?). Now, [Class] declaration bodies are either of the form [meth : type] or [{ meth : type ; ... }], distinguishing singleton "definitional" classes and inductive classes based on records. The constructor syntax is accepted ([meth1 : type1 | meth1 : type2]) but raises an error immediately, as support for defining a class by a general inductive type is not there yet (this is a bugfix!). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11679 85f007b7-540e-0410-9357-904b9bb8a0f7
* - configure: do not strip coqtop on Darwin so as to support dynamic loadingGravatar herbelin2008-12-12
| | | | | | | | | | | - configure: remove useless newline (hoping it is OK for everyone) - coqc: added option -no-glob in accordance with coqc -usage - coq_makefile: support for installation of all .cmo and all .cmxs in user-contrib git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11676 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformity with the rest of the StdLib : _symm --> _symGravatar letouzey2008-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11675 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed in bug in previous 11662 (incorrect with_evars flag in ↵Gravatar herbelin2008-12-12
| | | | | | descend_conjunction) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11670 85f007b7-540e-0410-9357-904b9bb8a0f7
* Structural definition of PositiveMap.foldGravatar glondu2008-12-11
| | | | | | | This definition makes it usable in fixpoints over inductive types based on PositiveMap.t . git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11668 85f007b7-540e-0410-9357-904b9bb8a0f7
* do not install coqchk cmi filesGravatar barras2008-12-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11666 85f007b7-540e-0410-9357-904b9bb8a0f7
* Make PositiveMap.xmapi structuralGravatar glondu2008-12-11
| | | | | | | | | With the previous definition, it was e.g. impossible to define a fixpoint for the inductive type: Inductive t : Set := T : PositiveMap.t t -> t. using PositiveMap.map. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11664 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug in 11662 (did not notice that dp_zenon.mll should be modified instead of Gravatar herbelin2008-12-10
| | | | | | | dp_zenon.ml) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11663 85f007b7-540e-0410-9357-904b9bb8a0f7
* About "apply in":Gravatar herbelin2008-12-09
| | | | | | | | | | | | | | | | | | - Added "simple apply in" (cf wish 1917) + conversion and descent under conjunction + contraction of useless beta-redex in "apply in" + support for open terms. - Did not solve the "problem" that "apply in" generates a let-in which is type-checked using a kernel conversion in the opposite side of what the proof indicated (hence leading to a potential unexpected penalty at Qed time). - When applyng a sequence of lemmas, it would have been nice to allow temporary evars as intermediate steps but this was too long to implement. Smoother API in tactics.mli for assert_by/assert_as/pose_proof. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11662 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix handling of [inverse] in setoid_rewrite, with an hopefully completeGravatar msozeau2008-12-08
| | | | | | | procedure. Brainstormed with Nicolas Tabareau. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11660 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix exponential behaviour of the typeclasses persistent objects. DropGravatar puech2008-12-06
| | | | | | | | | unused methods object. Matthieu please review this change (after monday), I might have introduced a bug in rebuild_instance. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11659 85f007b7-540e-0410-9357-904b9bb8a0f7
* Do not catch _all_ exceptions in setoid unification.Gravatar msozeau2008-12-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11658 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correct handling of defined methods (let-ins) in instance declarations.Gravatar msozeau2008-12-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11657 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix priority of the Leibniz Setoid instance to 10 (thanks to M. LassonGravatar msozeau2008-12-04
| | | | | | | for the report). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11656 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes for unification and substitution of metas under binders.Gravatar msozeau2008-12-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11655 85f007b7-540e-0410-9357-904b9bb8a0f7
* improved simplGravatar barras2008-12-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11653 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add new directory for pre-compilation of files needed for further tests.Gravatar herbelin2008-12-02
| | | | | | | Application to the test of notation import from within a section. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11652 85f007b7-540e-0410-9357-904b9bb8a0f7
* Miscellaneous fixes and improvements:Gravatar herbelin2008-12-02
| | | | | | | | | | | - Fixed a virtual bug of unification (ever occurs if w_unify called with a non-empty context of rel's, which is a priori uncommon). - Fixed Notation.out test. - Add better coqide error message in case editor is called on an unnamed file. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11650 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed kernel bug (de Bruijn) + test-suiteGravatar barras2008-12-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11646 85f007b7-540e-0410-9357-904b9bb8a0f7
* another bug with simplGravatar barras2008-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11644 85f007b7-540e-0410-9357-904b9bb8a0f7
* Inductive parameters: nicer doc examples and error messageGravatar letouzey2008-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11642 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test case for previous commit.Gravatar msozeau2008-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11641 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix (?) a pattern matching compilation problem: Gravatar msozeau2008-11-27
| | | | | | | | | | | | | | | | | << Axiom A : nat -> bool. Definition foo := match A 0 with | true => true | k => k end. Print foo. >> [A 0] is duplicated in the [k => k] branch! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11640 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 03:31:36 +0000