aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Fix Setoid documentation.Gravatar msozeau2009-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12421 85f007b7-540e-0410-9357-904b9bb8a0f7
* Local/Global revision 12418 continuedGravatar herbelin2009-10-26
| | | | | | | | - Fixing non-export of newly created Local Argument Scope. - Fixing bad discharge of local variables in nested sections (bug still exists in v8.2). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12420 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adapted test unfold.v after eq gets its argument maximally insertedGravatar herbelin2009-10-26
| | | | | | | (commit r12379). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12419 85f007b7-540e-0410-9357-904b9bb8a0f7
* New cleaning phase of the Local/Global option managementGravatar herbelin2009-10-26
| | | | | | | | | - Clarification and documentation of the different styles of Local/Global modifiers in vernacexpr.ml - Addition of Global in sections for Open/Close Scope. - Addition of Local for Ltac when not in sections. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12418 85f007b7-540e-0410-9357-904b9bb8a0f7
* New functors for gmap and gset.Gravatar soubiran2009-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12417 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restore (and test) broken chaining of lemmas in "apply in" in presenceGravatar herbelin2009-10-25
| | | | | | | | | of side conditions. Fix a small presentation issue in printing the "exists" tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12416 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed bug in Czar grammarGravatar corbinea2009-10-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12415 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add support for remaining side-conditions in "apply in as".Gravatar herbelin2009-10-25
| | | | | | | | | Tolerate that the place where to move an hypothesis with destruct is not "safe" if the lemma has dependent parameters inferred lately. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12412 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improved the treatment of Local/Global options (noneffective Local onGravatar herbelin2009-10-25
| | | | | | | | | | | | Implicit Arguments, Arguments Scope and Coercion fixed, noneffective Global in sections for Hints and Notation detected). Misc. improvements (comments + interpretation of Hint Constructors + dev printer for hint_db). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12411 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing XML doc (COQ_XML not working as an environment variable).Gravatar herbelin2009-10-24
| | | | | | | Fixing English grammar in inversion error message (reported in bug #2164). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12409 85f007b7-540e-0410-9357-904b9bb8a0f7
* First debug... the renaming of librairies was not working and auto/dn were ↵Gravatar soubiran2009-10-23
| | | | | | not taking in account equivalent names of inductive types. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12408 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix new instances that could easily make class resolution loop on Gravatar msozeau2009-10-22
| | | | | | | | unconstrained goals (e.g. PreOrder A ?). Allow the unconstrained use of [proper_reflexive] again. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12407 85f007b7-540e-0410-9357-904b9bb8a0f7
* This big commit addresses two problems:Gravatar soubiran2009-10-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 1- Management of the name-space in a modular development / sharing of non-logical objects. 2- Performance of atomic module operations (adding a module to the environment, subtyping ...). 1- There are 3 module constructions which derive equalities on fields from a module to another: Let P be a module path and foo a field of P Module M := P. Module M. Include P. ... End M. Declare Module K : S with Module M := P. In this 3 cases we don't want to be bothered by the duplication of names. Of course, M.foo delta reduce to P.foo but many non-logical features of coq do not work modulo conversion (they use eq_constr or constr_pat object). To engender a transparent name-space (ie using P.foo or M.foo is the same thing) we quotient the name-space by the equivalence relation on names induced by the 3 constructions above. To implement this, the types constant and mutual_inductive are now couples of kernel_names. The first projection correspond to the name used by the user and the second projection to the canonical name, for example the internal name of M.foo is (M.foo,P.foo). So: ************************************************************************************* * Use the eq_(con,mind,constructor,gr,egr...) function and not = on names values * ************************************************************************************* Map and Set indexed on names are ordered on user name for the kernel side and on canonical name outside. Thus we have sharing of notation, hints... for free (also for a posteriori declaration of them, ex: a notation on M.foo will be avaible on P.foo). If you want to use this, use the appropriate compare function defined in name.ml or libnames.ml. 2- No more time explosion (i hoppe) when using modules i have re-implemented atomic module operations so that they are all linear in the size of the module. We also have no more unique identifier (internal module names) for modules, it is now based on a section_path like mechanism => we have less substitutions to perform at require, module closing and subtyping but we pre-compute more information hence if we instanciate several functors then we have bigger vo. Last thing, the checker will not work well on vo(s) that contains one of the 3 constructions above, i will work on it soon... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12406 85f007b7-540e-0410-9357-904b9bb8a0f7
* MSetInterface: some explicit types to avoid Raw.t-instead-of-t effectGravatar letouzey2009-10-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12405 85f007b7-540e-0410-9357-904b9bb8a0f7
* Repaired bug #2165 (buggy coq example in Tactic Examples doc chapter)Gravatar herbelin2009-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12404 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added syntactic coloration for 'Function'.Gravatar gmelquio2009-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12403 85f007b7-540e-0410-9357-904b9bb8a0f7
* FSetCompat: a compatibility wrapper between FSets and MSetsGravatar letouzey2009-10-20
| | | | | | | | | | | | Thanks to the functors in FSetCompat, the three implementations of FSets (FSetWeakList, FSetList, FSetAVL) are just made of a few lines adapting the corresponding MSets implementation to the old interface. This approach breaks FSetFullAVL. Since this file is of little use for stdlib users, we migrate it into contrib Orsay/FSets. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12402 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merge SetoidList2 into SetoidList: forgotten reference to the removed fileGravatar letouzey2009-10-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12401 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merge SetoidList2 into SetoidList.Gravatar letouzey2009-10-19
| | | | | | | | | This file contains low-level stuff for FSets/FMaps. Switching it to the new version (the one using Equivalence and so on instead of eq_refl/eq_sym/eq_trans and so on) only leads to a few changes in FSets/FMaps that are minor and probably invisible to standard users. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12400 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed a notation bug when extending binder_constr with empty levelsGravatar herbelin2009-10-17
| | | | | | | | | (see Notations.v). Improved the "already occurs in a different scope" test and message. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12399 85f007b7-540e-0410-9357-904b9bb8a0f7
* OrderedType2 : trivial lemmas are turned into tests for order.Gravatar letouzey2009-10-16
| | | | | | | In particular we remove them from the hint db, a few autos become calls to order. Moreover, lt_antirefl --> lt_irrefl for uniformity. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12398 85f007b7-540e-0410-9357-904b9bb8a0f7
* Structure/OrderTac.v : highlight the "order" tactic by isolating it from ↵Gravatar letouzey2009-10-16
| | | | | | | | | | | | | | FSets, and improve it As soon as you have a eq, a lt and a le (that may be lt\/eq, or (complement (flip (lt))) and a few basic properties over them, you can instantiate functor MakeOrderTac and gain an "order" tactic. See comments in the file for the scope of this tactic. NB: order doesn't call auto anymore. It only searches for a contradiction in the current set of (in)equalities (after the goal was optionally turned into hyp by double negation). Thanks to S. Lescuyer for his suggestions about this tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12397 85f007b7-540e-0410-9357-904b9bb8a0f7
* note for later : when the tag table is shared, never, ever create twoGravatar vgross2009-10-16
| | | | | | tags with the same name. This fixes file opening. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12396 85f007b7-540e-0410-9357-904b9bb8a0f7
* typo in doc of Extraction BlacklistGravatar letouzey2009-10-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12394 85f007b7-540e-0410-9357-904b9bb8a0f7
* MSetInterface: (W)Raw2Sets splitted in 2 (helps a future commit by Elie)Gravatar letouzey2009-10-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12393 85f007b7-540e-0410-9357-904b9bb8a0f7
* OrderedType2.order is slightly weaker since last commit, adapt accordinglyGravatar letouzey2009-10-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12392 85f007b7-540e-0410-9357-904b9bb8a0f7
* OrderedType2.order : fix the last fix (a fail at the wrong place)Gravatar letouzey2009-10-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12391 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug in typeclass resolution discoverd by Eeelis van der Weegen:Gravatar msozeau2009-10-15
| | | | | | | | the wrong evar_defs was used when checking if an evar was to be resolved or not. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12390 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo in last commitGravatar letouzey2009-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12389 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improved tactic "order" in OrderedTypeGravatar letouzey2009-10-14
| | | | | | | | | | | | | | | | | | | I forgot to mention in last commit message about MSets that the corresponding OrderedType2 comes with a redesigned "order" tactic. It should now be complete for its purpose (that is solve systems of (in)equations of variables over == < <= <>). Non-linear matching is cool, I love Ltac :-). Unlike the old "order", this new version is meant to completely solve the goal or fail. Speed might be an issue for big systems, but in pratice it is quite efficient on the examples encountered in FSets. This commit: - propagages this new "order" to the original OrderedType.v file used for the old FSet. - fixes a bug : the ltac loop shouldn't fail otherwise strange backtrack occurs. I hate Ltac :-( git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12388 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made implicit arguments of Operators_Properties.v localGravatar herbelin2009-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12387 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typos.Gravatar gmelquio2009-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12386 85f007b7-540e-0410-9357-904b9bb8a0f7
* Better handling of emphasis.Gravatar msozeau2009-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12385 85f007b7-540e-0410-9357-904b9bb8a0f7
* MSets: a new generation of FSetsGravatar letouzey2009-10-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Same global ideas (in particular the use of modules/functors), but: - frequent use of Type Classes inside interfaces/implementation. For instance, no more eq_refl/eq_sym/eq_trans, but Equivalence. A class StrictOrder for lt in OrderedType. Extensive use of Proper and rewrite. - now that rewrite is mature, we write specifications of set operators via iff instead of many separate requirements based on ->. For instance add_spec : In y (add x s) <-> E.eq y x \/ In x s. Old-style specs are available in the functor Facts. - compare is now a pure function (t -> t -> comparison) instead of returning a dependent type Compare. - The "Raw" functors (the ones dealing with e.g. list with no sortedness proofs yet, but morally sorted when operating on them) are given proper interfaces and a generic functor allows to obtain a regular set implementation out of a "raw" one. The last two points allow to manipulate set objects that are completely free of proof-parts if one wants to. Later proofs will rely on type-classes instance search mechanism. No need to emphasis the fact that this new version is severely incompatible with the earlier one. I've no precise ideas yet on how allowing an easy transition (functors ?). For the moment, these new Sets are placed alongside the old ones, in directory MSets (M for Modular, to constrast with forthcoming CSets, see below). A few files exist currently in version foo.v and foo2.v, I'll try to merge them without breaking things. Old FSets will probably move to a contrib later. Still to be done: - adapt FMap in the same way - integrate misc stuff like multisets or the map function - CSets, i.e. Sets based on Type Classes : Integration of code contributed by S. Lescuyer is on the way. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12384 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #2162 and a name clashing bug in generalized binders.Gravatar msozeau2009-10-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12383 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix a typo(?) in previous commitGravatar letouzey2009-10-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12382 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed clash names in Relations (see bug report #2152) and make namesGravatar herbelin2009-10-08
| | | | | | | | in Relation_Operators.v and Operators_Properties.v more uniform in general. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12381 85f007b7-540e-0410-9357-904b9bb8a0f7
* Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'Gravatar letouzey2009-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12380 85f007b7-540e-0410-9357-904b9bb8a0f7
* Implicit argument of Logic.eq become maximally insertedGravatar letouzey2009-10-08
| | | | | | | | | This allow in particular to write eq instead of (@eq _) in signatures of morphisms. I dont really see how this could break existing code, no change in the stdlib was mandatory. We'll check the contribs tomorrow... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12379 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed a bug introduced in revision 12265.Gravatar herbelin2009-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12378 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix for missing hypotesae in XML proof tree export.Gravatar cek2009-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12377 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed installation of Coqide interface/library files (bug #2147).Gravatar gmelquio2009-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12376 85f007b7-540e-0410-9357-904b9bb8a0f7
* Relaxed error severity when encountering unknown library objects or tacticGravatar gmelquio2009-10-06
| | | | | | | extensions. This makes it possible to load .vo compiled with a nonstandard toplevel, e.g. ssreflect, which defines new tactics and new hint databases. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12375 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correctly do backtracking during type class resolution even if only newGravatar msozeau2009-10-05
| | | | | | | | | | existentials are generated (at last!). The code simply keeps failure continuations and apply them if needed. Fix bottomup and topdown rewrite strategies that looped. Use auto introduction flag for typeclass instances as well. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12374 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert "kills the old backtracking framework and replaces it with"Gravatar vgross2009-10-05
| | | | | | This reverts commit 33545cc88bf4b4e19b222afd2d1d264bcba97838. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12373 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changed the way to support compatibility with previous versions.Gravatar herbelin2009-10-04
| | | | | | | | Compatibility version is now a global parameter that every feature can individually browse. This avoids having to keep the names of options synchronous in their respective files and in now-removed file coqcompat.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12372 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removal of trailing spaces.Gravatar serpyc2009-10-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12371 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some new lemmas on max and min and a fix for a wrongly stated lemma in r12358.Gravatar herbelin2009-10-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12370 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed small name freshness bug in Functional Scheme ("Heq" name wasGravatar herbelin2009-10-03
| | | | | | | not refreshed late enough). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12369 85f007b7-540e-0410-9357-904b9bb8a0f7
* A few additions in Min.v.Gravatar herbelin2009-10-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12368 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-30 03:37:19 +0000