diff --git a/.gitignore b/.gitignore
index a5f73a2c..631803fc 100644
--- a/.gitignore
+++ b/.gitignore
@@ -16,6 +16,7 @@ coqproofs
 *.glob
 *.vo[ks]
 *.vo
+GIT_TIPS.md
 
 *.v
 !goeland.v
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index a3632354..556f836d 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -9,8 +9,8 @@ wish to contribute to Goéland, you should start by
 you can work on on your feature/bug fix/enhancement in your local repository.
 
 Once you deem your work satisfactory, you should [open a pull
-request](https://github.com/GoelandProver/Goeland/compare) **targeting
-master**. Then, one of the maintainer will review your code as soon as
+request](#working-with-pull-requests) targeting
+master. Then, one of the maintainer will review your code as soon as
 possible. If you have no feedback for a few days, do not hesitate to ping one of
 them. The current maintainers are: @jcailler, @jrosain.
 
@@ -20,8 +20,8 @@ maintainers will trigger the CI when he sees fit. You may check soundness
 locally by running the `ci-soundness` target of the [devtools](devtools)
 folder. Note that it is **not** the maintainer's responsibility to make your
 modifications compatible with the master's branch. If there are any conflicts,
-you are expected to solve them by *rebasing your branch on top of upstream's
-master*.
+you are expected to solve them by rebasing your branch on top of upstream's
+master.
 
 If you are solving a bug referenced in the issue tracker, do not forget to link
 it in the PR.
@@ -41,12 +41,39 @@ flag in order for them to panic and you to have a backtrace.
 
 ## For Maintainers
 
-By default, a pull request that modifies the go source code has the `needs:ci` label. You
-may trigger CI jobs by adding the label `request:ci`, which will remove the `needs:ci` if
-it succeeds. Every time a new push is done on the pull request's branch, the `needs:ci`
-label will reappear. Try to never remove this label by hand, it is good practice to
-request a successful full ci run before merging the PR into the master's branch. Moreover,
-it is your responsibility to put the right `part:` and `kind:` labels.
+By default, a pull request that modifies the go source code has the `needs:ci`
+label. You may trigger CI jobs by adding the label `request:ci`, which will
+remove the `needs:ci` if it succeeds. Every time a new push is done on the pull
+request's branch, the `needs:ci` label will reappear. Avoid removing this label
+by hand, and always prefer requesting the CI. 
 
-Once you approve the modifications, you should add the target milestone (i.e.,
-which version of Goéland should include the patch) before merging.
+It is the maintainer’s responsibility to:
+- add the appropriate `part:` and `kind:` labels,
+- approve changes once ready,
+- assign a milestone indicating the target Goéland release (i.e., which version of Goéland should include the patch) before merging.
+
+
+## Working with Pull Requests
+
+Before opening a pull request, make sure your branch is up-to-date with the master's branch of `GoelandProver/Goeland` or at least mergeable without conflicts. You can update your branch using:
+
+```bash
+git fetch remote/master
+git rebase remote/master
+```
+
+where `remote` is the name of the remote fetching `git@github.com:GoelandProver/Goeland.git` (which can be found using `git remote -v`)
+
+1. Check that the branch with your new features/bug fixes is up-to-date.
+2. Open a pull request [here](https://github.com/GoelandProver/Goeland/compare) targeting `master`.
+3. Give an explicit name to your pull request, e.g., `Fix nil pointer exception when skolemizing` or `Add a library of maps`.
+4. If your pull request is a bug fix, be sure to add `Closes: #???` where `#???` is the issue you are closing/fixing.
+5. In any case, describe briefly what you did in the code and what are the technical points that might be of interest / things you are not sure about on the design you chose.
+6. If you have updated the test-suite, list all the updates you did.
+7. In particular, if you fixed a bug, you should have updated the test suite with the problem `.p` where the bug appeared (or a minimized version) in the `devtools/test-suite/bugs` folder and named it `bug_???.p` (or `bug_???-n.p` if there are multiple bugs).
+8. If you introduce a new feature, you might add problems in the `devtool/test-suite/basic` or `devtool/test-suite/proofs` folders, and update the unit tests.
+9. Once everything is clear, you can submit your PR and wait until a reviewer gets back to you.
+
+Maintainers may ask you to squash your commits to simplify the history. However, squashing is not always required — in some cases, preserving the commit history is preferred. Wait for a maintainer's guidance before squashing. 
+
+Subsequently, if you have any further question, the reviewer will answer them.