aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Collapse)AuthorAge
* 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-10-09
|\|
| * 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.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
|\|
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
|\ \
| | * 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
| |
* | Merge remote-tracking branch 'origin/v8.5' into trunkGravatar Hugo Herbelin2015-09-09
|\|
| * 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
| |
* | Adding a proof of surjective pairing on vectors.Gravatar Hugo Herbelin2015-08-29
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-08-05
|\|
| * 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
| |
* | Merge remote-tracking branch 'forge/v8.5'Gravatar Pierre Boutillier2015-06-22
|\|
| * The "on_last_hyp" tactic now behaves as it should.Gravatar Cyprien Mangin2015-06-12
| |
* | 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.
| * Mark PreOrder as a consequence of Equivalence. (Fix bug #4213)Gravatar Guillaume Melquiond2015-05-12
| |
* | Tentatively setting cons and Some with 1st implicit argument maximalGravatar Hugo Herbelin2015-05-09
| | | | | | | | (see #3695).
* | 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.
| * 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.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-03-11
|\|
| * 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
| |
* | Merge branch 'v8.5' into trunkGravatar Pierre Letouzey2015-03-06
|\|
| * MMapPositive: another implementation of MMapsGravatar Pierre Letouzey2015-03-06
| |
* | Merge branch 'v8.5' into trunkGravatar Pierre Letouzey2015-03-05
|\|
| * 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".
* | 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".
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-02-26
|\|
| * 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).
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-13 06:07:58 +0000