Stream: math-comp analysis

Topic: math-comp/analysis#187

Cyril Cohen (May 07 2020 at 22:06):

@affeldt-aist do you mind if I squash both our commits and put myself as co-authored-by, it makes no sense to keep the history... single commits are not compiling anymore anyway.

Reynald Affeldt (May 07 2020 at 22:08):

please, go ahead

Cyril Cohen (May 08 2020 at 16:19):

are you still working on this PR ?

Reynald Affeldt (May 08 2020 at 16:22):

well, I did promise to do my homework by monday, true that I didn't have much time since yesterday :-(

Cyril Cohen (May 08 2020 at 16:23):

May I ask what you are doing on it so that we do not collide?

Reynald Affeldt (May 08 2020 at 16:25):

(I think I did push something yesterday evening...)

Reynald Affeldt (May 08 2020 at 16:26):

ah!

Reynald Affeldt (May 08 2020 at 16:27):

we lost one commit!

Cyril Cohen (May 08 2020 at 16:27):

oooh

Cyril Cohen (May 08 2020 at 16:27):

sorry....

Cyril Cohen (May 08 2020 at 16:28):

do you know the commit number ?

Reynald Affeldt (May 08 2020 at 16:31):

I still had my emacs buffer

Reynald Affeldt (May 08 2020 at 16:32):

I was about to tackle near_non(de|in)creasing_is_cvg to be precise.

Cyril Cohen (May 08 2020 at 16:33):

ok, thanks, I will do a fixup with it

Reynald Affeldt (May 08 2020 at 16:35):

Then I was planning to fix cesaroand produce a few lemmas dual of already existing lemmas

Reynald Affeldt (May 08 2020 at 16:36):

and use this experience to feed the contributing guide

Cyril Cohen (May 08 2020 at 16:40):

ok!

Reynald Affeldt (May 08 2020 at 16:40):

sorry, I pushed in a hurry and the CI didn't go through, let me fix this

Cyril Cohen (May 08 2020 at 16:41):

I will merge math-comp/analysis#202 and rebase sequences on it

Cyril Cohen (May 08 2020 at 16:41):

affeldt-aist said:

sorry, I pushed in a hurry and the CI didn't go through, let me fix this

I noticed already and it is almost fixed

Reynald Affeldt (May 08 2020 at 16:44):

ok, I let you do that (strangely it was compiling in emacs, something changed under my feet)

Cyril Cohen (May 08 2020 at 16:44):

yes, I accidentally removed image_inj

Cyril Cohen (May 08 2020 at 16:45):

(+ bounded changed a few other things under your feet)

Cyril Cohen (May 08 2020 at 16:45):

I hope I did not loose more

Cyril Cohen (May 08 2020 at 16:45):

could you give me the commit number ?

Cyril Cohen (May 08 2020 at 16:45):

git rev-parse HEAD

Reynald Affeldt (May 08 2020 at 16:46):

d46f2364841b3cd0ceb85fee76d37a62a3f50a9d (yesterday's commit that disappeared)

Cyril Cohen (May 08 2020 at 16:51):

a last rebase and I give it back

Last updated: Apr 19 2024 at 13:02 UTC