aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Lists
Commit message (Collapse)AuthorAge
* Fix 3 unused-intro-pattern warnings in stdlib.Gravatar Théo Zimmermann2017-03-14
|
* Remove v62 from stdlib.Gravatar Théo Zimmermann2016-10-24
| | | | | This old compatibility hint database can be safely removed now that coq-contribs do not depend on it anymore.
* Move vector/list compat notations to their relevant filesGravatar Jason Gross2016-09-29
| | | | | | | Since edb55a94fc5c0473e57f5a61c0c723194c2ff414 landed, compat notations no longer modify the parser in non-compat-mode, so we can do this without breaking Ltac parsing. Also update the related test-suite files.
* Remove spaces from around list notationsGravatar Jason Gross2016-09-26
|
* Giving a more natural semantics to injection by default.Gravatar Hugo Herbelin2016-06-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | There were three versions of injection: 1. "injection term" without "as" clause: was leaving hypotheses on the goal in reverse order 2. "injection term as ipat", first version: was introduction hypotheses using ipat in reverse order without checking that the number of ipat was the size of the injection (activated with "Unset Injection L2R Pattern Order") 3. "injection term as ipat", second version: was introduction hypotheses using ipat in left-to-right order checking that the number of ipat was the size of the injection and clearing the injecting term by default if an hypothesis (activated with "Set Injection L2R Pattern Order", default one from 8.5) There is now: 4. "injection term" without "as" clause, new version: introducing the components of the injection in the context in left-to-right order using default intro-patterns "?" and clearing the injecting term by default if an hypothesis (activated with "Set Structural Injection") The new versions 3. and 4. are the "expected" ones in the sense that they have the following good properties: - introduction in the context is in the natural left-to-right order - "injection" behaves the same with and without "as", always introducing the hypotheses in the goal what corresponds to the natural expectation as the changes I made in the proof scripts for adaptation confirm - clear the "injection" hypothesis when an hypothesis which is the natural expectation as the changes I made in the proof scripts for adaptation confirm The compatibility can be preserved by "Unset Structural Injection" or by calling "simple injection". The flag is currently off.
* Revert "Temporary hack to compensate missing comma while re-printing tactic"Gravatar Hugo Herbelin2016-04-27
| | | | This reverts commit 3a2753bedf43a8c7306b1b3fc9cb37aafb78ad7a.
* Temporary hack to compensate missing comma while re-printing tacticGravatar Hugo Herbelin2016-04-27
| | | | "exists c1, c2".
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-02-21
|\
| * Fixing bug #4582: cannot override notation [ x ].Gravatar Pierre-Marie Pédrot2016-02-19
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-17
|\|
| * Proof using: do not clear unused section hyps automaticallyGravatar Enrico Tassi2015-12-15
| | | | | | | | | | | | The option is still there, but not documented since it is too dangerous. Hints and type classes instances are not taking cleared variables into account.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-15
|\|
| * Fix some typos.Gravatar Guillaume Melquiond2015-10-14
| |
| * Fix some typos.Gravatar Guillaume Melquiond2015-10-13
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-08-05
|\|
| * Remove some outdated files and fix permissions.Gravatar Guillaume Melquiond2015-07-31
| |
* | Merge v8.5 into trunkGravatar Hugo Herbelin2015-05-15
|\| | | | | | | | | | | | | Conflicts: tactics/eauto.ml4 (merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)
| * List.nth_error directly produces Some/None instead of value/errorGravatar Pierre Letouzey2015-05-12
| | | | | | | | | | | | | | | | | | | | | | | | List.nth_error and List.hd_error were the only remaining places in the whole stdlib to use type "Exc" instead of "option" directly. So let's simplify things and use option everywhere. In particular, during teaching sessions about lists, we won't have anymore to explain the (lack of) difference between Exc,value,error and option,Some,None. This might cause a few incompatibilities in proof scripts, if they syntactically expect "value" or "error" to occur, but this should hopefully be very rare and quite easy to fix.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-05-05
|\|
| * Giving to "subst" a more natural semantic (fixing #4214) by using allGravatar Hugo Herbelin2015-05-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | equalities in configurations like x=y x=z === P(x,y,z) where it now produces === P(z,z,z) In particular (equations are processed from most ancient to most recent). Thanks to this, a "repeat subst" can just be a "subst" in List.v. Incidentally: moved a nf_enter to enter in subst_one, since the latter is normally called from other tactics having normalized evars.
* | Merge branch 'v8.5' into trunkGravatar Pierre Letouzey2015-04-09
|\|
| * Prove [map_ext] using [map_ext_in].Gravatar Nickolai Zeldovich2015-04-09
| | | | | | | | Since [map_ext_in] is more general, no need to have the same proof twice.
| * Add a [map_ext_in] lemma to List.v.Gravatar Nickolai Zeldovich2015-04-09
| | | | | | | | | | | | Slightly broader version of the existing [map_ext]: two [map] expressions are equal if their respective functions agree on all arguments that are in the list being mapped.
| * Introducing MMaps, a modernized FMaps.Gravatar Pierre Letouzey2015-03-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | NB: this is work-in-progress, there is currently only one provided implementation (MMapWeakList). In the same spirit as MSets w.r.t FSets, the main difference between MMaps and former FMaps is the use of a new version of OrderedType (see Orders.v instead of obsolete OrderedType.v). We also try to benefit more from recent notions such as Proper. For most function specifications, the style has changed : we now use equations over "find" instead of "MapsTo" predicates, whenever possible (cf. Maps in Compcert for a source of inspiration). Former specs are now derived in FMapFacts, so this is mostly a matter of taste. Two changes inspired by the current Maps of OCaml: - "elements" is now "bindings" - "map2" is now "merge" (and its function argument also receives a key). We now use a maximal implicit argument for "empty".
* | Introducing MMaps, a modernized FMaps.Gravatar Pierre Letouzey2015-03-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | NB: this is work-in-progress, there is currently only one provided implementation (MMapWeakList). In the same spirit as MSets w.r.t FSets, the main difference between MMaps and former FMaps is the use of a new version of OrderedType (see Orders.v instead of obsolete OrderedType.v). We also try to benefit more from recent notions such as Proper. For most function specifications, the style has changed : we now use equations over "find" instead of "MapsTo" predicates, whenever possible (cf. Maps in Compcert for a source of inspiration). Former specs are now derived in FMapFacts, so this is mostly a matter of taste. Two changes inspired by the current Maps of OCaml: - "elements" is now "bindings" - "map2" is now "merge" (and its function argument also receives a key). We now use a maximal implicit argument for "empty".
* | Add two lemmas about firstn to the List standard library.Gravatar Sébastien Hinderer2015-01-16
| |
* | Lemmas related to the firstn function over lists.Gravatar Sébastien Hinderer2015-01-16
| |
* | ListSet: follow-up of Sebastien's last commitGravatar Pierre Letouzey2015-01-16
| | | | | | | | | | More results on set_remove, in particular explicit the NoDup pre-condition. Show that NoDup is preserved by other operations.
* | Work in progress on listset.Gravatar Sébastien Hinderer2015-01-16
|/
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Use [Proof using] to make sure that [List.in_flat_map] doesn't grab too many ↵Gravatar Arnaud Spiwack2014-12-28
| | | | | section variable. For some reason, the subproofs solved by [auto] had started using [Hfinjective] from the section context.
* Adds two lemmas about hderror to the List standard library.Gravatar Sébastien Hinderer2014-12-18
|
* Implement the nodup function on lists and prove associated results.Gravatar Sébastien Hinderer2014-12-18
|
* Lists: enhanced version of Seb's last commit on Exists/ForallGravatar Pierre Letouzey2014-12-18
|
* Lists: a few results on Exists and Forall and a bit of code cleanup.Gravatar Sébastien Hinderer2014-12-18
|
* List.v: sequel to Sebastien's commit (some cosmetics + a few shorter proofs)Gravatar Pierre Letouzey2014-12-11
|
* First series of results on lists.Gravatar Sébastien Hinderer2014-12-11
|
* Clarifying the role of ListSet.v in the library, compared to otherGravatar Hugo Herbelin2014-11-18
| | | | finite set libraries.
* Improving printing of "[]" (nil) in spite of the risk of collisionGravatar Hugo Herbelin2014-08-05
| | | | with possible further use of token "[]" + slight restructuration.
* Testing a replacement of "cut" by "enough" on a couple of test files.Gravatar Hugo Herbelin2014-08-05
|
* More proofs independent of the names generated by induction/elim overGravatar Hugo Herbelin2014-08-05
| | | | a dependent elimination principle for Prop arguments.
* Adding a generalized version of fold_Equal to FMapFacts.Gravatar Pierre Courtieu2014-07-31
| | | | | | | This commit should be refactored by Pierre L. if he thinks this should replace the previous version of fold_Equal, for now it is a different lemma fold_Equal2. Same for the Section addded to SetoiList, it should maybe replace the previous one.
* Avoid using a deprecated lemma in the standard library.Gravatar Guillaume Melquiond2014-06-26
|
* Make standard library independent of the names generated byGravatar Hugo Herbelin2014-06-04
| | | | | induction/elim over a dependent elimination principle for Prop arguments.
* Making those proofs which depend on names generated for the argumentsGravatar Hugo Herbelin2014-06-01
| | | | | | | | | in Prop of constructors of inductive types independent of these names. Incidentally upgraded/simplified a couple of proofs, mainly in Reals. This prepares to the next commit about using names based on H for such hypotheses in Prop.
* Try a new way of handling template universe levelsGravatar Matthieu Sozeau2014-05-06
|
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
| | | | | | | | | | | | | | | | | | - Remove Universe Polymorphism flags everywhere. - Properly infer, discharge template arities and fix substitution inside them (kernel code to check for correctness). - Fix tactics that were supposing universe polymorphic constants/inductives to be parametric on that status. Required to make interp_constr* return the whole evar universe context now. - Fix the univ/level/instance hashconsing to respect the fact that marshalling doesn't preserve sharing, sadly losing most of its benefits. Short-term solution is to add hashes to these for faster comparison, longer term requires rewriting all serialization code. Conflicts: kernel/univ.ml tactics/tactics.ml theories/Logic/EqdepFacts.v
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
| | | | | | | | | | | | latent universes. Now the universes in the type of a definition/lemma are eagerly added to the environment so that later proofs can be checked independently of the original (delegated) proof body. - Fixed firstorder, ring to work correctly with universe polymorphism. - Changed constr_of_global to raise an anomaly if side effects would be lost by turning a polymorphic constant into a constr. - Fix a non-termination issue in solve_evar_evar. -
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 09:32:35 +0000