aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Collapse)AuthorAge
* Remove the "exists" overrides from Program. (Fix bug #4360)Gravatar Guillaume Melquiond2015-10-07
|
* Univs: add Strict Universe Declaration option (on by default)Gravatar Matthieu Sozeau2015-10-07
| | | | | | | | | This option disallows "declare at first use" semantics for universe variables (in @{}), forcing the declaration of _all_ universes appearing in a definition when introducing it with syntax Definition/Inductive foo@{i j k} .. The bound universes at the end of a definition/inductive must be exactly those ones, no extras allowed currently. Test-suite files using the old semantics just disable the option.
* Remove Print Universe directive.Gravatar Matthieu Sozeau2015-10-02
|
* Universes: enforce Set <= i for all Type occurrences.Gravatar Matthieu Sozeau2015-10-02
|
* Add compatibility files (feature 4319)Gravatar Jason Gross2015-09-30
|
* Emphasizing that eta for vectors is an instance of caseS, as pointedGravatar Hugo Herbelin2015-09-08
| | | | | | out to me by Pierre B. Also extending use of bullets in Vectors where relevant.
* Minor modifications to WeakFanTheorem.Gravatar Hugo Herbelin2015-09-08
|
* Adding a proof of eta on Vector.t of non-zero size.Gravatar Hugo Herbelin2015-09-08
|
* Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
| | | | | | | | | | | | | | | | | | | | | | Sorry so much. Reverted: 707bfd5719b76d131152a258d49740165fbafe03. 164637cc3a4e8895ed4ec420e300bd692d3e7812. b9c96c601a8366b75ee8b76d3184ee57379e2620. 21e41af41b52914469885f40155702f325d5c786. 7532f3243ba585f21a8f594d3dc788e38dfa2cb8. 27fb880ab6924ec20ce44aeaeb8d89592c1b91cd. fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c. d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962. 6737055d165c91904fc04534bee6b9c05c0235b1. 342fed039e53f00ff8758513149f8d41fa3a2e99. 21525bae8801d98ff2f1b52217d7603505ada2d2. b78d86d50727af61e0c4417cf2ef12cbfc73239d. 979de570714d340aaab7a6e99e08d46aa616e7da. f556da10a117396c2c796f6915321b67849f65cd. d8226295e6237a43de33475f798c3c8ac6ac4866. fdab811e58094accc02875c1f83e6476f4598d26.
* Adding a notation { x & P } for { x : _ & P }.Gravatar Hugo Herbelin2015-08-02
|
* Remove some outdated files and fix permissions.Gravatar Guillaume Melquiond2015-07-31
|
* The "on_last_hyp" tactic now behaves as it should.Gravatar Cyprien Mangin2015-06-12
|
* 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.
* Mark PreOrder as a consequence of Equivalence. (Fix bug #4213)Gravatar Guillaume Melquiond2015-05-12
|
* 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.
* 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.
* Fix instances of universe-polymorphic generalized rewriting to avoidGravatar Matthieu Sozeau2015-04-09
| | | | spurious quantification on unused universes.
* MMapAVL: some improved proofs + fix a forgotten AdmittedGravatar Pierre Letouzey2015-04-02
|
* MMapAVL: implementing MMapInterface via AVL treesGravatar Pierre Letouzey2015-04-02
|
* ZArith/Int.v: some modernizationsGravatar Pierre Letouzey2015-04-02
|
* MMapPositive: some improvementsGravatar Pierre Letouzey2015-04-02
| | | | | Most of them are backports of improvements already there in FSetPositive when compared with the original FMapPositive file.
* Accomodating #4166 (providing "Require Import OmegaTactic" as aGravatar Hugo Herbelin2015-04-01
| | | | replacement for 8.4's "Require Omega").
* Fix various typos in documentationGravatar Matěj Grabovský2015-03-31
| | | | Closes #57.
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
| | | | | | | | | | | | | | | - no more inconsistent Axiom in the Prelude - STM can now process Admitted proofs asynchronously - the quick chain can stock "Admitted" jobs in .vio files - the vio2vo step checks the jobs but does not stock the result in the opaque tables (they have no slot) - Admitted emits a warning if the proof is complete - Admitted uses the (partial) proof term to infer section variables used (if not given with Proof using), like for Qed - test-suite: extra line Require TestSuite.admit to each file making use of admit - test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to find TestSuite.admit
* Add some missing Proof keywords.Gravatar Guillaume Melquiond2015-03-06
|
* MMapPositive: another implementation of MMapsGravatar Pierre Letouzey2015-03-06
|
* MMaps again : adding MMapList, an implementation by ordered listGravatar Pierre Letouzey2015-03-05
|
* 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".
* Revert "Fixing bug #4035 (support for dependent destruction within ltac code)."Gravatar Maxime Dénès2015-02-26
| | | | | | | | | This reverts commit 4e6c9891140932f452bb5ac8960d597b0b5fde1d, which was breaking compatibility because one could no longer use names of foralls in the goal without introducting them. Probably not good style, but it did break many existing developments including CompCert. Closes #4093 but reopens #4035.
* Reorder the steps of the easy tactic. (Fix for bug #2630)Gravatar Guillaume Melquiond2015-02-25
| | | | | | | Due to the way it was laid out, the tactic could prove neither (Zle x x) nor (P /\ Q -> P) nor (P |- P /\ True) yet it could prove (Zle x x /\ True) and (P /\ Q |- P).
* Fix some typos in comments.Gravatar Guillaume Melquiond2015-02-23
|
* Fixing bug #4035 (support for dependent destruction within ltac code).Gravatar Hugo Herbelin2015-02-16
|
* dependent destruction: Fix (part of) bug #3961, by fixing dependent *Gravatar Matthieu Sozeau2015-02-14
| | | | generalizing * which was broken since 8.4.
* There was one more universe needed due to the use of now ↵Gravatar Matthieu Sozeau2015-01-18
| | | | | | non-universe-polymorphic ID, fixing the script results in 3 universes for the stdlib again.
* Correct restriction of vm_compute when handling universe polymorphicGravatar Matthieu Sozeau2015-01-15
| | | | | | | | | | definitions. Instead of failing with an anomaly when trying to do conversion or computation with the vm's, consider polymorphic constants as being opaque and keep instances around. This way the code is still correct but (obviously) incomplete for polymorphic definitions and we avoid introducing an anomaly. The patch does nothing clever, it only keeps around instances with constants/inductives and compile constant bodies only for non-polymorphic definitions.
* Remove typeclass opaque directive, some proofs in the stdlib rely on it ↵Gravatar Matthieu Sozeau2015-01-15
| | | | being transparent
* Optionally allow eta-conversion during unification for type classes.Gravatar Matthieu Sozeau2015-01-15
| | | | | | Off by default as it can be backwards-incompatible (e.g. produces loop in the library without an additional Typeclasses Opaque directive in RelationPairs).
* 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.
* Forbid Require inside interactive modules and module types.Gravatar Maxime Dénès2014-12-25
| | | | | | | Fixes #3379 and part of #3363. Also avoids fragile code propagating required libraries when closing an interactive module. Had to fix a few occurrences in std lib.
* 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
|
* Failing on unbound notation variable in notation level modifiersGravatar Hugo Herbelin2014-12-15
| | | | | | | + consequences of this check on the standard library (moved the no-op in Notation modifiers to what there were supposed to do; these are anyway local notations, so compatibility is safe - please AS or PL, amend if needed).
* 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
|
* Added an arithmetical characterization of the hypothesis of WKL.Gravatar Hugo Herbelin2014-12-01
|
* Clarifying the role of ListSet.v in the library, compared to otherGravatar Hugo Herbelin2014-11-18
| | | | finite set libraries.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 13:16:37 +0000