aboutsummaryrefslogtreecommitdiff
path: root/theories/FSets/FMapFullAVL.v
AgeCommit message (Collapse)Author
2020-11-16Explicitly annotate all hint declarations of the standard library.Pierre-Marie Pédrot
By default Coq stdlib warnings raise an error, so this is really required.
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2019-10-22FSets: do not use “omega”Vincent Laporte
2019-10-04[Stdlib] OrderedType: do not pollute the “core” hint databaseVincent Laporte
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-03-30Error when [foo.(bar)] is used with nonprojection [bar]Gaëtan Gilbert
(warn if bar is a nonprimitive projection)
2018-12-19Put #[universes(template)] on all auto template spots in stdlibGaëtan Gilbert
2018-11-14Deprecate hint declaration/removal with no specified databaseMaxime Dénès
Previously, hints added without a specified database where implicitly put in the "core" database, which was discouraged by the user manual (because of the lack of modularity of this approach).
2018-09-10Deprecate romega in favor of lia.Vincent Laporte
2018-02-27Update headers following #6543.Théo Zimmermann
2017-06-14Prelude : no more autoload of plugins extraction and recdefPierre Letouzey
The user now has to manually load them, respectively via: Require Extraction Require Import FunInd The "Import" in the case of FunInd is to ensure that the tactics functional induction and functional inversion are indeed in scope. Note that the Recdef.v file is still there as well (it contains complements used when doing Function with measures), and it also triggers a load of FunInd.v. This change is correctly documented in the refman, and the test-suite has been adapted.
2014-09-27Keyed unification option, compiling the whole standard libraryMatthieu Sozeau
(but deactivated still). Set Keyed Unification to activate the option, which changes subterm selection to _always_ use full conversion _after_ finding a subterm whose head/key matches the key of the term we're looking for. This applies to rewrite and higher-order unification in apply/elim/destruct. Most proof scripts already abide by these semantics. For those that don't, it's usually only a matter of using: Declare Equivalent Keys f g. This make keyed unification consider f and g to match as keys. This takes care of most cases of abbreviations: typically Def foo := bar and rewriting with a bar-headed lhs in a goal mentioning foo works once they're set equivalent. For canonical structures, these hints should be automatically declared. For non-global-reference headed terms, the key is the constructor name (Sort, Prod...). Evars and metas are no keys. INCOMPATIBILITIES: In FMapFullAVL, a Function definition doesn't go through with keyed unification on.
2014-06-26Avoid using a deprecated lemma in the standard library.Guillaume Melquiond
2013-01-18Unset Asymmetric Patternspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16129 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-05Open Local Scope ---> Local Open Scope, same with Notation and aliiletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15517 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-08Made option "Automatic Introduction" active by default before too manyherbelin
people use the undocumented "Lemma foo x : t" feature in a way incompatible with this activation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13090 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
- Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-08Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12380 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-28Fix the stdlib doc compilation + switch all .v file to utf8letouzey
1) compilation of Library.tex was failing on a "Ext_" in Diaconescu.v In fact coqdoc was trying to recognize the end of a _emphasis_ and hence inserted a bogus }. For the moment I've enclosed the phrase with [ ], but this emphasis "feature" of coqdoc seems _really_ easy to broke. Matthieu ? 2) By the way, this Library document was made from latin1 and utf8 source file, hence bogus characters. All .v containing special characters are converted to utf8, and their first line is now mentionning this. (+ killed some old french comments and some other avoidable special characters). PLEASE: let's stick to this convention and avoid latin1, at least in .v files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12363 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-28ZArith/Int: no need to load romega here (but rather in FullAVL)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12027 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-03New file FMapFullAVL containing the balancing proofs about FMapAVL:letouzey
As for FSetAVL vs. FSetFullAVL, preservation of the balancing of trees is not necessary anymore for just fulfilling the Map interface. But we still want theses proofs to exists somewhere, since they ensure the correct efficiency of the FMapAVL operations. In addition, FSetFullAVL also contains the non-structural, ocaml-faithful version of compare. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10748 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:51:48 +0000