aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2008-12-18FSets: integration of suggestions by P. Casteran and S. Lescuyerletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11698 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-18- Fixed cutrewrite bug #2021 introduced in commit 11662 (as a sideherbelin
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
2008-12-17Avoid printing that extraction has created file Foo when it's not the caseletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11695 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-17Better compatibility after commit 11693 by adding an alias ↵letouzey
OrderedTypeFacts.eq_dec git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11694 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-17FSet/OrderedType now includes an eq_dec, and hence become an extension of ↵letouzey
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
2008-12-17Sequel of 11697: repair coqtop.byte when contribs are statically linked ↵letouzey
(+minor improvements) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11692 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-16Extraction Blacklist : a new command for avoiding conflicts with existing filesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11690 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-16Extraction: also comply to Set Printing Width when producing external filesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11688 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-16Take advantage of natdynlink when available: almost all contribs become ↵letouzey
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
2008-12-16Move FunctionalExtensionality to Logic/ (someone please check that themsozeau
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
2008-12-16Finish fix for the treatment of [inverse] in [setoid_rewrite], making amsozeau
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
2008-12-16Fix for syntax changes in test-suite scripts.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11684 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-15Add some unicode symbols from japanese CJC (request by Y. Regis-Gianas)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11683 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-14Fix looping class resolution bug discovered by B. Aydemir and use themsozeau
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
2008-12-14Fixes in the type classes documentation:msozeau
- 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
2008-12-14Generalized binding syntax overhaul: only two new binders: `() and `{},msozeau
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
2008-12-12- configure: do not strip coqtop on Darwin so as to support dynamic loadingherbelin
- 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
2008-12-12Uniformity with the rest of the StdLib : _symm --> _symletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11675 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-12Fixed in bug in previous 11662 (incorrect with_evars flag in ↵herbelin
descend_conjunction) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11670 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-11Structural definition of PositiveMap.foldglondu
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
2008-12-11do not install coqchk cmi filesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11666 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-11Make PositiveMap.xmapi structuralglondu
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
2008-12-10Bug in 11662 (did not notice that dp_zenon.mll should be modified instead of herbelin
dp_zenon.ml) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11663 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-09About "apply in":herbelin
- 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
2008-12-08Fix handling of [inverse] in setoid_rewrite, with an hopefully completemsozeau
procedure. Brainstormed with Nicolas Tabareau. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11660 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-06Fix exponential behaviour of the typeclasses persistent objects. Droppuech
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
2008-12-04Do not catch _all_ exceptions in setoid unification.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11658 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-04Correct handling of defined methods (let-ins) in instance declarations.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11657 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-04Fix priority of the Leibniz Setoid instance to 10 (thanks to M. Lassonmsozeau
for the report). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11656 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-04Fixes for unification and substitution of metas under binders.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11655 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-03improved simplbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11653 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-02Add new directory for pre-compilation of files needed for further tests.herbelin
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
2008-12-02Miscellaneous fixes and improvements:herbelin
- 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
2008-12-02fixed kernel bug (de Bruijn) + test-suitebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11646 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-28another bug with simplbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11644 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-28Inductive parameters: nicer doc examples and error messageletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11642 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-27Test case for previous commit.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11641 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-27Fix (?) a pattern matching compilation problem: msozeau
<< 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
2008-11-27fixed non-exhaustive pattern matchingbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11638 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-27fixed bug 1791: simpl was performing eta expansionbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11636 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-27added tests for hyps reorderingbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11635 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-27fixing problem with CompCert: reordering resulting from tac change was not ↵barras
closed w.r.t. dependencies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11634 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-26closed bug 1898: fold x in x; added a reordering primitive tacticbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11633 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-26closed bug 1898: fold x in x; added a reordering primitive tacticbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11632 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-25correction bug 1997.soubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11630 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-24eventually fixing r11612barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11626 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-24amelioration mineur du comportement de Functionjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11625 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-23first attempt to allow Function to deal with dependent pattern matching. ↵jforest
This Functionnality is VERY VERY experimental and only works with non recursive functions and structurally defined function git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11624 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-23- Synchronized subst_object with load_object (load_and_subst_objects)herbelin
and set Declare ML Module as a regular substitutive object so that Declare ML Module is treated at the right place in the order of appearance of substitutive declarations of a required module. - Note: The full load/import mechanism for modules is not so clear: the Require part of a Require Import inside a module is set outside the module at module closing but the Import part remains inside (why not to put the "special" objects in the module too?); moreover the "substitute" and "keep" objects of a module are desynchronised at module closing (is that really harmless/necessary?). - Treatment of .cmxs targets in coq_makefile and in coqdep. - Better make clean in coq_makefile generated makefiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11623 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-23Fine-tuning rewriting from "eq_true b": using <- to rewrite true to bherbelin
(if ever necessary). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11621 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-25 23:48:28 +0000