aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Collapse)AuthorAge
* Fix to previous commit (ClassicalFacts.v).Gravatar Hugo Herbelin2015-12-05
|
* Adding proofs on the relation between excluded-middle and minimization.Gravatar Hugo Herbelin2015-12-05
| | | | | | | In particular, a proof of the equivalence of excluded-middle and an unrestricted principle of minimization. Credits to Arnaud Spiwack for the ideas and formalizations of the proofs.
* Experimenting removing strong normalization of the mid-statement in tactic cut.Gravatar Hugo Herbelin2015-12-05
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-29
|\
| * Univs: entirely disallow instantiation of polymorphic constants withGravatar Matthieu Sozeau2015-11-27
| | | | | | | | | | | | | | | | | | Prop levels. As they are typed assuming all variables are >= Set now, and this was breaking an invariant in typing. Only one instance in the standard library was used in Hurkens, which can be avoided easily. This also avoids displaying unnecessary >= Set constraints everywhere.
* | Updating Compat85.v after bd1c97653 on bracketing last or-andGravatar Hugo Herbelin2015-11-10
| | | | | | | | introduction pattern by default.
* | Adding an amazing property of Prop.Gravatar Hugo Herbelin2015-11-07
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-05
|\|
| * Update compatibility file for some of bug #4392Gravatar Jason Gross2015-11-03
| | | | | | | | | | | | | | | | | | | | | | | | | | Now doing ```coq Tactic Notation "left" "~" := left. Tactic Notation "left" "*" := left. ``` will no longer break the `left` tactic in Coq 8.4. List obtained via ``` grep -o '^ \[[^]]*\]' tactics/coretactics.ml4 | sed s'/^ \[ \(.*\) \]/Tactic Notation \1 := \1./g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\) \(constr\|bindings\|constr_with_bindings\|quantified_hypothesis\|ne_hyp_list\)(\([^)]*\))/\1 \3/g' ```
* | 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
| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 02:17:15 +0000