aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)Author
2017-09-15Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" ↵Maxime Dénès
work better on them
2017-09-03Addressing BZ#5713 (classical_left/classical_right artificially restricted).Hugo Herbelin
As explained in BZ#5713 report, the requirement for a non-empty context is not needed, so we remove it.
2017-08-29A little reorganization of notations + a fix to #5608.Hugo Herbelin
- Formerly, notations such as "{ A } + { B }" were typically split into "{ _ }" and "_ + _". We keep the split only for parsing, which is where it is really needed, but not anymore for interpretation, nor printing. - As a consequence, one notation string can give rise to several grammar entries, but still only one printing entry. - As another consequence, "{ A } + { B }" and "A + { B }" must be reserved to be used, which is after all the natural expectation, even if the sublevels are constrained. - We also now keep the information "is ident", "is binder" in the "key" characterizing the level of a notation.
2017-08-21Ensuring all .v files end with a newline to make "sed -i" work better on them.Hugo Herbelin
2017-07-26Merge PR #882: Adding a V8.7 compatibility version number.Maxime Dénès
2017-07-26Merge PR #885: Removing a dummy parameter in some FMapPositive statements.Maxime Dénès
2017-07-26Merge PR #845: Add Z.mod_div lemma to standard library.Maxime Dénès
2017-07-21Adding a V8.7 compatibility version number.Hugo Herbelin
2017-07-16Removing a dummy parameter in some FMapPositive statements.Hugo Herbelin
The statements xelements_bits_lt_1 and xelements_bits_lt_2 had an unexpected extra dependency due to a name collision with a section variable.
2017-07-05Fix typo in documentation for identityTej Chajed
Fixes Coq bug 5635 (https://coq.inria.fr/bugs/show_bug.cgi?id=5635).
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-29Fix Zmod_div.Russell O'Connor
2017-06-29Use forall for consistencyroconnor-blockstream
2017-06-29Add Z.mod_div lemma to standard library.Russell O'Connor
2017-06-26Merge PR#826: Put plugin exports in the right compatibility fileMaxime Dénès
2017-06-23Merge PR#794: Cleanup of ltac cmxsMaxime Dénès
2017-06-22Put plugin exports in the right compatibility fileJason Gross
This closes [bug #5607](https://coq.inria.fr/bugs/show_bug.cgi?id=5607). PR #220 put the exports in the wrong compat files, presumably because it was originally targeted to version 8.6, and this wasn't updated when it was retargeted to version 8.7.
2017-06-15plugins/ltac : avoid spurious .cmxs filesPierre Letouzey
In the previous setting, all plugins/ltac/*.cmxs except ltac_plugin.cmxs (for instance coretactics.cmxs, g_auto.cmxs, ...) were utterly bogus : - wrong -for-pack used for their inner .cmx - dependency over modules not provided (for instance Tacenv, that ends up being a submodule of the pack ltac_plugin). But we were lucky, those files were actually never loaded, thanks to the several DECLARE PLUGIN inside coretactics and co, that end up in ltac_plugin, and hence tell Coq that these modules are already known, preventing any attempt to load them. Anyway, this commit cleans up this mess (thanks PMP for the help)
2017-06-15Merge PR#375: DeprecationMaxime Dénès
2017-06-14Merge PR#753: Fix bug 5026 (the stdlib shouldn't define inconsistent notations).Maxime Dénès
2017-06-14Prelude : no more autoload of plugins extraction and recdefPierre Letouzey
The user now has to manually load them, respectively via: Require Extraction Require Import FunInd The "Import" in the case of FunInd is to ensure that the tactics functional induction and functional inversion are indeed in scope. Note that the Recdef.v file is still there as well (it contains complements used when doing Function with measures), and it also triggers a load of FunInd.v. This change is correctly documented in the refman, and the test-suite has been adapted.
2017-06-14Remove deprecated options from the standard library.Guillaume Melquiond
2017-06-14Remove support for Coq 8.4.Guillaume Melquiond
2017-06-14Merge PR#498: Bignums as a separate opam packageMaxime Dénès
2017-06-13Merge PR#385: Equality of sigma typesMaxime Dénès
2017-06-13BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Pierre Letouzey
See now https://github.com/coq/bignums Int31 is still in the stdlib. Some proofs there has be adapted to avoid the need for BigNumPrelude.
2017-06-10Remove remaining vo.itarget files (obsolete since PR #499)Pierre Letouzey
2017-06-08Fix bug 5026 (the stdlib shouldn't define inconsistent notations).Théo Zimmermann
2017-06-01drop vo.itarget files and compute the corresponding the corresponding values ↵Matej Kosik
automatically instead
2017-05-28More uniform indentation of sigma lemmasJason Gross
2017-05-28Give explicit proof terms to proj2_sig_eq etc.Jason Gross
2017-05-28Use the rew dependent notation in ex, ex2 proofsJason Gross
2017-05-28Make theorems about ex equality QedJason Gross
As requested in https://github.com/coq/coq/pull/384#issuecomment-303809461
2017-05-28Make new proofs of equality QedJason Gross
As requested in https://github.com/coq/coq/pull/384#issuecomment-303809461
2017-05-28Add some more comments about sigma equalitiesJason Gross
Forwards/backwards reasoning thoughts come from https://github.com/coq/coq/pull/385#discussion_r111008347
2017-05-28Remove motive argument from [rew dependent]Jason Gross
2017-05-28Use a local [rew dependent] notationJason Gross
2017-05-28Add forward-chaining versions: [eq_sig*_uncurried]Jason Gross
2017-05-28Use notation for sigTJason Gross
2017-05-28Remove reference to [IsIso]Jason Gross
2017-05-28Use notations for [sig], [sigT], [sig2], [sigT2]Jason Gross
2017-05-28Use extended notation for ex, ex2 typesJason Gross
2017-05-28Replace [ex'] with [ex]Jason Gross
The ' was originally denoting that we were taking in the projections and applying the constructor in the conclusion, rather than taking in the bundled versions and projecting them out (because the projections don't exist for [ex] and [ex2]). But we don't have versions like this for [sig] and [sigT] and [sigT2] and [sig2], so we might as well not add the ' to the [ex] and [ex2] versions.
2017-05-28Use [rew_] instead of [eq_rect_] prefixJason Gross
As per Hugo's request.
2017-05-28Add equality lemmas for sig2 and sigT2Jason Gross
2017-05-28Add lemmas for ex2Jason Gross
2017-05-28Use [rew] notations rather than [eq_rect]Jason Gross
As per Hugo's suggestion in https://github.com/coq/coq/pull/384#issuecomment-264891011
2017-05-28Add an [inversion_sigma] tacticJason Gross
This tactic does better than [inversion] at sigma types.
2017-05-28Add lemmas about equality of sigma typesJason Gross
2017-05-28Use [rew_] instead of [eq_rect_] prefixJason Gross
As per Hugo's request.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 06:22:30 +0000