aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* list, length, app are migrated from List to DatatypesGravatar letouzey2009-11-02
| | | | | | | | | | | | | | | | | This allows easier handling of dependencies, for instance RelationClasses won't have to requires List (which itself requires part of Arith, etc). One of the underlying ideas is to provide setoid rewriting in Init someday. Thanks to some notations in List, this change should be fairly transparent to the user. For instance, one could see that List.length is a notation for (Datatypes.)length only when doing a Print List.length. For these notations not to be too intrusive, they are hidden behind an explicit Export of Datatypes at the end of List. This isn't very pretty, but quite handy. Notation.ml is patched to stop complaining in the case of reloading the same Delimit Scope twice. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12452 85f007b7-540e-0410-9357-904b9bb8a0f7
* Undo 12432 which caused an exponential behavior at Requires. Compilation ↵Gravatar puech2009-10-30
| | | | | | time should be back to normal. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12451 85f007b7-540e-0410-9357-904b9bb8a0f7
* Attempt to capture on time unification errors for "with" bindings.Gravatar herbelin2009-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12450 85f007b7-540e-0410-9357-904b9bb8a0f7
* Take constraints into account in the "instantiate" tacticGravatar herbelin2009-10-30
| | | | | | | | (building an example that needs it to do). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12449 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added Coqide highlighting for extraction vernacular.Gravatar gmelquio2009-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12448 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed 'dest' from keyword highlighting.Gravatar gmelquio2009-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12447 85f007b7-540e-0410-9357-904b9bb8a0f7
* Hopefully improved layout of fix guardness error message.Gravatar herbelin2009-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12445 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix flat_map definition so that it plays nicely with fixGravatar glondu2009-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12444 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed some typos in the reference manual.Gravatar gmelquio2009-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12443 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revision 12439 continued, printing part (notations to names behaveGravatar herbelin2009-10-29
| | | | | | | | like the name they refer to). Fixing buggy test-suite implicit.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12442 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug in dnet.ml, which missed some results when filtering one term ↵Gravatar puech2009-10-29
| | | | | | | | | | against many patterns. Conflicts: lib/dnet.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12441 85f007b7-540e-0410-9357-904b9bb8a0f7
* Integrate a few improvements on typeclasses and Program from the equations ↵Gravatar msozeau2009-10-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | branch and remove equations stuff which moves to a separate plugin. Classes: - Ability to define classes post-hoc from constants or inductive types. - Correctly rebuild the hint database associated to local hypotheses when they are changed by a [Hint Extern] in typeclass resolution. Tactics and proofs: - Change [revert] so that it keeps let-ins (but not [generalize]). - Various improvements to the [generalize_eqs] tactic to make it more robust and produce the smallest proof terms possible. Move [specialize_hypothesis] in tactics.ml as it goes hand in hand with [generalize_eqs]. - A few new general purpose tactics in Program.Tactics like [revert_until] - Make transitive closure well-foundedness proofs transparent. - More uniform testing for metas/evars in pretyping/unification.ml (might introduce a few changes in the contribs). Program: - Better sorting of dependencies in obligations. - Ability to start a Program definition from just a type and no obligations, automatically adding an obligation for this type. - In compilation of Program's well-founded definitions, make the functional a separate definition for easier reasoning. - Add a hint database for every Program populated by [Hint Unfold]s for every defined obligation constant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12440 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made that notations to names behave like the names they refer to wrtGravatar herbelin2009-10-28
| | | | | | | | | implicit arguments and scope (use Implicit Arguments or Arguments Scope commands instead if not the desired behaviour). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12439 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed a bug when reporting unexisting reference to an inductiveGravatar herbelin2009-10-28
| | | | | | | | (introduced in r12323). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12438 85f007b7-540e-0410-9357-904b9bb8a0f7
* Clarification in commentsGravatar glondu2009-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12437 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove old compatibility stuff (Tacred.nf)Gravatar glondu2009-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12436 85f007b7-540e-0410-9357-904b9bb8a0f7
* Make usage of Dyn explicitGravatar glondu2009-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12435 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backport fix for indexing of sorts which collapse every Type occurrenceGravatar msozeau2009-10-28
| | | | | | | into a SortLabel None. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12434 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo in the refmanGravatar puech2009-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12433 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix incorrect registration of objects in libtypes.ml when defining a module.Gravatar puech2009-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12432 85f007b7-540e-0410-9357-904b9bb8a0f7
* Same as commit 12430 but with the good version of the function iter_all_segmentGravatar soubiran2009-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12431 85f007b7-540e-0410-9357-904b9bb8a0f7
* From now SearchAbout requests search also inside INCLUDE libobject.Gravatar soubiran2009-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12430 85f007b7-540e-0410-9357-904b9bb8a0f7
* Module type expressions of the form (Fsig X) with Definition foo := bar are ↵Gravatar soubiran2009-10-28
| | | | | | | | | | now accepted. +svn:ignore property on folders git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12429 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a new vernacular command for controling implicit generalization ofGravatar msozeau2009-10-27
| | | | | | | | | | | | | variables with syntax: [Local?|Global] Generalizable Variable(s)? [all|none|id1 idn]. By default no variable is generalizable, so this patch breaks backward compatibility with files that used implicit generalization (through Instance declarations for example). To get back the old behavior, one just needs to use [Global Generalizable Variables all]. Make coq_makefile more robust using [mkdir -p]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12428 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes around typeclasses:Gravatar msozeau2009-10-27
| | | | | | | | | | | | | | - Correct discharge/classify/rebuild for instances. Semantic of Global/Local: local by default in sections, global by default in modules. - Fix the discrimination net's handling of type universes, let the unification do it. - Correct the typeclass resolution tactic so that when extern tactics themselves launch class resolution we don't duplicate work. Problem reported by Arthur Chargueraud. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12427 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added option --external to coqdoc to bind an url to an external library.Gravatar herbelin2009-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12426 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation of the Local and Global modifiers.Gravatar herbelin2009-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12425 85f007b7-540e-0410-9357-904b9bb8a0f7
* fix previous commitGravatar corbinea2009-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12424 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed czar bug with parametric inductivesGravatar corbinea2009-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12423 85f007b7-540e-0410-9357-904b9bb8a0f7
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 05:21:42 +0000