aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Collapse)AuthorAge
* 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.
* Enforcing a stronger difference between the two syntaxes "simplGravatar Hugo Herbelin2014-11-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | reference" and "simpl pattern" in the code (maybe we should have merged them instead, but I finally decided to enforce their difference, even if some compatibility is to be preversed - the idea is that at some time "simpl reference" would only call a weak-head simpl (or eventually cbn), leading e.g. to reduce 2+n into S(1+n) rather than S(S(n)) which could be useful for better using induction hypotheses. In the process we also implement the following: - 'simpl "+"' is accepted to reduce all applicative subterms whose head symbol is written "+" (in the toplevel scope); idem for vm_compute and native_compute - 'simpl reference' works even if reference has maximally inserted implicit arguments (this solves the "simpl fst" incompatibility) - compatibility of ltac expressions referring to vm_compute and native_compute with functor application should now work (i.e. vm_compute and native_compute are now taken into account in tacsubst.ml) - for compatibility, "simpl eq" (assuming no maximal implicit args in eq) or "simpl @eq" to mean "simpl (eq _ _)" are still allowed. By the way, is "mul" on nat defined optimally? "3*n" simplifies to "n+(n+(n+0))". Are there some advantages of this compared to have it simplified to "n+n+n" (i.e. to "(n+n)+n").
* Improving elimination with indices, getting rid of intrusive residualGravatar Hugo Herbelin2014-11-02
| | | | local definitions...
* Supporting "at occs" as a short-hand for "in |- * at occs" in "destruct".Gravatar Hugo Herbelin2014-11-02
|
* Make sure that Logic/ExtensionalityFacts gets compiled.Gravatar Guillaume Melquiond2014-10-27
|
* Fix some typos.Gravatar Guillaume Melquiond2014-10-27
|
* Fix some typos in comments.Gravatar Guillaume Melquiond2014-10-27
|
* EqdepFacts: generalize statements which were wrongly restricted to Prop.Gravatar Arnaud Spiwack2014-10-22
|
* Fixing typo absorption (bug #3751).Gravatar Hugo Herbelin2014-10-22
|
* Revert "Essai où assert_style n'est utilisé que si pas visuellement une ↵Gravatar Hugo Herbelin2014-10-17
| | | | | | équation;" which was committed by mistake. This reverts commit a53b44aa042cfded28c34205074f194de7e2e4ee.
* Essai où assert_style n'est utilisé que si pas visuellement une équation;Gravatar Hugo Herbelin2014-10-17
|
* ConstructiveEpsilon: simplify the before_witness type using non-uniform ↵Gravatar Arnaud Spiwack2014-10-16
| | | | parameters.
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 03:55:34 +0000