aboutsummaryrefslogtreecommitdiff
path: root/CREDITS
AgeCommit message (Collapse)Author
2020-10-02{new,setoid_}ring -> ringMaxime Dénès
I believe this renaming makes it easier for new contributors to discover the code of `ring`.
2019-10-09A few fixes to the CREDITS file.Théo Zimmermann
Move to the right alphabetical ordering, fix dates, institutions. Also add Jim, but not all the other missing people because I officially renounce to keeping this file up-to-date.
2019-09-01Vectors: lemmas about uncons and splitAtYishuai Li
Co-authored-by: Konstantinos Kallas <konstantinos.kallas@hotmail.com>
2019-06-17Clean-up CREDITS file.Théo Zimmermann
Remove mentions of removed plugins. Remove copyright years to avoid them going out of sync. Fix explanation of the license of the documentation.
2019-06-05Add Andreas Lynge to CREDITSAndreas Lynge
2019-06-03Fix affiliation and ordering in CREDITSTalia Ringer
2019-05-22unified style for new hooks and old hooksTalia Ringer
2019-04-30fix `simpl_rel` and notations, `{pred T}` alias, `nonPropType` interfaceGeorges Gonthier
** Changed definition of `simpl_rel` to `T -> `simpl_pred T`, so that `inE` will now expand `a \in r b`, when `r := [rel x y | R]` to `R{b/x, a/y}`, as the expanding coercion is now only inserted in the _last_ application. The old definition made it possible to have a `simpl_rel >-> rel` coercion that does not block expansion, but this can now be achieved more economically with the `Arguments … /.` annotation. ** Deleted the `[rel of P]` notation which is no longer needed with the new `simpl_rel` definition, and was broken anyway. ** Added `relpre f R` definition of functional preimage of a notation. ** `comp` and `idfun` are now proper definitions, using the `Arguments … /.` annotation to specify simplification on application. ** Added `{pred T}` syntax for the alias of `pred T` in the `pred_sort` coercion class; deleted the `pred_class` alias: one should either use `pred_sort` in `Coercion` declarations, or `{pred T}` in type casts. Used `{pred T}` as appropriate in localised predicate (`{in …, …}`) theory. Extended and corrected `pred` coercion internal documentation. ** Simplified the `predType` structure by removing the redundant explicit `mem_pred` subfield, and replacing it with an interlocked projection; deleted `mkPredType`, now replaced by `PredType`. ** Added (and extensively documented) a `nonPropType` interface matching types that do _not_ have sort `Prop`, and used it to remove the non-standard maximal implicits annotation on `Some_inj` introduced in #6911 by @anton-trumov; included `test-suite` entry for `nonPropType`. ** Documented the design of the four structures used to control the matching of `inE` and related predicate rewriting lemmas; added `test-suite` entry covering the `pred` rewriting control idioms. ** Used `only printing` annotations to get rid of token concatenation hacks. ** Fixed boolean and general `if b return t then …` notation so that `b` is bound in `t`. This is a minor source of incompatibility for misuses of this syntax when `b` is _not_ bound in `t`, and `(if b then …) : t` should have been used instead. ** Reserved all `ssreflect`, `ssrfun` and `ssrbool` notation at the top of the file, adding some printing boxes, and removing some spurious `[pred .. => ..]` reserved notation. ** Fixed parsing precedence and format of `<hidden n>` notation, and declared and put it in an explicit `ssr_scope`. ** Used module-and-functor idiom to ensure that the `simpl_pred T >- pred T` _and_ `simpl_pred T >-> {pred T}` coercions are realised by the _same_ Gallina constant. ** Updated `CREDITS`. The policy implied by this PR: that `{pred T}` should systematically be used as the generic collective predicate type, was implemented in MathComp math-comp/math-comp#237. As a result `simpl_pred >-> pred_sort` coercions became more frequent, as it turned out they were not, as incorrectly stated in `ssrbool` internal comments, impossible: while the `simplPredType` canonical instance does solve all `simpl_pred T =~= pred_sort ?pT` instances, it does _not_ solve `simpl_pred T =~= {pred T}`, and so the coercion will be used in that case. However it appeared that having two different coercion constants confused the SSReflect keyed matching heuristic, hence the fix introduced here. This has entailed some rearrangement of `ssrbool`: the large `Predicates` section had to be broken up as the module-functor idiom for aliasing coercions cannot be used inside a section.
2018-12-10Merge PR #7221: The usual order of strings.Hugo Herbelin
2018-11-27Added two proofs to the Lists library. The first, Forall_inv_tail, extends ↵llee454@gmail.com
Forall_inv to assert that a property that is true for every element of a list is true for every element in the tail of the list. The second, Exists_impl, parallels Forall_impl and proves that if there exists an element in a list that satisfies a given predicate, and the predicate implies another proposition, then there exists an element in the list that satisfies the implied proposition. Both of these proofs fill natural gaps within the List library.
2018-11-22The usual order of strings.Yao Li
2018-11-01Fix alphabetical orderVincent Semeria
2018-11-01Fix creditsVincent Semeria
2018-11-01proof that R is uncountableVincent Semeria
2018-09-12Remove quote pluginMaxime Dénès
As far as I know, this plugin is untested and barely maintained. I don't think it has real use cases any more, so let's move it out from the repo and see if somebody wants to take over and maintain it. We also remove the documentation, which was telling our users to look at ring to see an example of reification done using quote, when in fact it wasn't using it anymore.
2018-07-17Remove fourier pluginMaxime Dénès
As stated in the manual, the fourier tactic is subsumed by lra.
2018-04-15Simplify CircleCI scriptYishuai Li
2018-04-11Add credits related to the Sphinx migration.Théo Zimmermann
Closes #7209.
2018-02-21Update CREDITS.Théo Zimmermann
In particular, add a mention of SSReflect.
2017-09-05Update CREDITS on a best-effort basis.Théo Zimmermann
And with help from https://github.com/coq/coq/graphs/contributors
2016-06-15ssrmatching: giving proper credits to the original author(s)Enrico Tassi
Following CeCILL-B 5.3.2, we are allowed to redistribute the software under the same license of Coq as long as we credit.
2015-01-15Hugo put me in credits, but I was already there :)Maxime Dénès
2015-01-13Tentatively updating credits while remaining brief.Hugo Herbelin
2015-01-12Add myself to credits.Maxime Dénès
2015-01-12Update credits.Guillaume Melquiond
2014-12-09Switch the few remaining iso-latin-1 files to utf8Pierre Letouzey
2012-05-29Vernacexpr is now a mli-only file, locality stuff now in locality.mlletouzey
Adds a directory ./intf for pure interfaces. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15367 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-25Fixed #2789.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15360 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-25Version number, copyright, credits: missing updates.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14862 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-03plugin groebner updated and renamed as nsatz; first version of the doc of ↵pottier
nsatz in the refman git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13056 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-09Update of credits filesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13004 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-22Backport from v8.2 branch of 11986 (interpretation of quantifiedherbelin
hypotheses in induction, unbalanced parenthesis in ltac call stack printer) and 12003 (late update of CREDITS) + update of magic numbers (using a somehow arbitrary value between the 8.2 magic numbers and the possibly forthcoming 8.3 magic numbers). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12007 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ↵letouzey
user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-19MAJ créditsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10948 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-16first-order --> firstorder (kills a warning about not being a valid id)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10805 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-15- Un peu de doc, préparation du CHANGES pour la release.herbelin
- Re-restriction de inversion (après la correction des bugs - et notamment du "Unknown meta" qui apparaissait parfois -, inversion devenait capable d'agir sur des buts non atomiques, ce qui crée quelques incompatibilités, typiquement dans CoRN où inversion est utilisé dans un rôle de discriminate; en attendant de voir, on revient à la sémantique initiale). - Généralisation de Local/Global dans Implicit Arguments pour avoir un fonctionnement plus uniforme et plus facile à documenter. - Code mort (clenv.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10796 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-30typoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9321 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-27Restriction au implémenteursherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9293 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-26MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9282 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-16Typo dans CREDITSnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8822 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-14mise a jour creditscpaulin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8716 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-14MAJ 8.1herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8709 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-09Référence pour IntMapherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7364 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-09Créditherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6089 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-12MAJ techniqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5890 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-17CREDITSmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5514 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-16Mise a jour ZArith/Cregutmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5508 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-15Mise a jour CREDITS en vue copyrightmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5490 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-04Added credits for jprover.huang
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2609 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-17MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2402 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:55:21 +0000