diff --git a/dev/git-hooks/pre-commit b/dev/git-hooks/pre-commit.sh
similarity index 62%
rename from dev/git-hooks/pre-commit
rename to dev/git-hooks/pre-commit.sh
index 36353a8d1a7c53153e9482ef9e40fc4510f1f3cf..4eaa0428ca6da4b9d88592ca08bc7622cdc05f4d 100755
--- a/dev/git-hooks/pre-commit
+++ b/dev/git-hooks/pre-commit.sh
@@ -1,5 +1,4 @@
 #!/bin/bash
-# -*- mode: bash
 ##########################################################################
 #                                                                        #
 #  This file is part of Frama-C.                                         #
@@ -22,21 +21,26 @@
 #                                                                        #
 ##########################################################################
 
-if git rev-parse --verify HEAD >/dev/null 2>&1
-then
-    against=HEAD
-else
-    # Initial commit: diff against an empty tree object
-    against=4b825dc642cb6eb9a060e54bf8d69288fbee4904
-fi
+# Examples of installation of this pre-commit hook (client side):
+# - cp ./dev/git-hooks/pre-commit.sh .git/hooks/pre-commit
+# - (cd .git/hooks/ && ln -s ../../dev/git-hooks/pre-commit.sh pre-commit)
+
+# Note:
+# - that checks the unstaged version of the files and these files are
+#   only commited with a `git commit -a` command.
+# - so, a `git commit` command may  checks the wrong version of a file.
+
+echo "Pre-commit Hook..."
 
-if git config --get frama-c.makelevel > /dev/null 2>&1 ; then
-  MAKELEVEL=-j$(git config --int --get frama-c.makelevel);
-else
-  MAKELEVEL=-j4;
+# Extract the files that have both an unstaged version and a staged one.
+UNSTAGED="git diff --name-status"
+STAGED="git diff --name-status --cached"
+(($UNSTAGED ; $STAGED) | sed "s:^.::" | sort -u) | diff - <(($UNSTAGED ; $STAGED) | sed "s:^.::" | sort)
+if [ "$?" != "0" ]; then
+    echo "WARNING: These previous files are both unstaged and in the index."
+    echo "         They will be verified only for a 'git commit -a' command."
 fi
 
-MANUAL_ML_FILES=\
-$(git diff-index --name-only --diff-filter d $against | \
-    grep -e '^src/.*\.mli\?$' | tr '\n' ' ') \
-make ${MAKELEVEL} lint
+# Verifies the current version of files
+make lint.before-commit-a
+make check-headers.before-commit-a
diff --git a/share/Makefile.headers b/share/Makefile.headers
index 7783e0955e2a1acbe1660f842cf723b9766b4931..8b243dae3572ba7dee6db4460a360ca5783018bc 100644
--- a/share/Makefile.headers
+++ b/share/Makefile.headers
@@ -30,7 +30,9 @@
 # Must be unset (for external plugins) and set (for FRAMA-C kernel)
 FRAMAC_HDRCK?=
 
-# Can be set to no
+HDRCK?=frama-c-hdrck
+
+# Can be set to no/yes
 # - yes: adds "-exit-on-warning" option to "frama-c-hdrck"
 HEADER_STRICT?=yes
 
@@ -67,6 +69,13 @@ HEADER_SAVE_SPEC?=no
 # Extra parameters for "frama-c-hdrck"
 HDRCK_EXTRA?=
 
+##########################################################################
+## Tools
+
+GIT  ?= git
+DUNE ?= dune
+TEE  ?= tee
+
 ##########################################################################
 ## Command used to execute hdrck
 
@@ -74,113 +83,116 @@ HDRCK_EXTRA?=
 ifeq ($(FRAMAC_HDRCK),)
 
 # HDRCK is external
-HDRCK:= frama-c-hdrck
+HDRCK.CMD:= $(HDRCK)
 
 else
 
 # HDRCK is internal
-HDRCK:= dune exec --root $(FRAMAC_HDRCK_SRC) -- frama-c-hdrck
+HDRCK.CMD:= $(DUNE) exec --root $(FRAMAC_HDRCK_SRC) -- $(HDRCK)
 
-$(FRAMAC_HDRCK): $(FRAMAC_HDRCK_SRC)/hdrck.ml
-	dune build --root $(FRAMAC_HDRCK_SRC) hdrck.exe
+$(FRAMAC_HDRCK): tools/hdrck/hdrck.ml
+	$(DUNE) build --root $(FRAMAC_HDRCK_SRC) hdrck.exe
 
 endif
 
-HDRCK_OPTS:= --stdin
+HDRCK.OPTS:= --stdin
 
 ######################################################################
 ## Identifies how to get the header specification (from git/find/cat)
-## and updates HDRCK_OPTS variable
+## and updates HDRCK.OPTS variable
+
+HDRCK.FILE_LIST=$(GIT) ls-files -z
+HDRCK.FILE_ATTR=$(GIT) check-attr --stdin -z header_spec
 
 ifeq ($(HEADER_SPEC),)
 
-HEADER_HAS_GIT:=$(wildcard .git)
-ifneq ($(HEADER_HAS_GIT),)
+HDRCK.HAS_GIT:=$(wildcard .git)
+ifneq ($(HDRCK.HAS_GIT),)
 
 # From git (including git work-trees)
-HDRCK_SPEC:= git ls-files -z | git check-attr --stdin -z header_spec
-HDRCK_OPTS+= -z
+HDRCK.SPEC:=$(HDRCK.FILE_LIST) | $(HDRCK.FILE_ATTR)
+HDRCK.OPTS+= -z
 
 else
 
 # Note: in such a case, GIT is required...
-HDRCK_SPEC:=
+HDRCK.SPEC:=
 
-endif # HEADER_HAS_GIT
+endif # HDRCK.HAS_GIT
 
 else # HEADER_SPEC
 
 ifeq ($(HEADER_SAVE_SPEC),yes)
 
-HEADER_HAS_GIT:=$(wildcard .git)
-ifneq ($(HEADER_HAS_GIT),)
+HDRCK.HAS_GIT:=$(wildcard .git)
+ifneq ($(HDRCK.HAS_GIT),)
 
 # From git (including git work-trees)
-HDRCK_SPEC:= git ls-files -z | git check-attr --stdin -z header_spec | tee $(HEADER_SPEC)
-HDRCK_OPTS+= -z
+HDRCK.SPEC:= $(HDRCK.FILE_LIST) | $(HDRCK.FILE_ATTR) | $(TEE) $(HEADER_SPEC)
+HDRCK.OPTS+= -z
 
 else
 
 # Note: in such a case, GIT is required...
-HDRCK_SPEC:=
+HDRCK.SPEC:=
 
-endif # HEADER_HAS_GIT
+endif # HDRCK.HAS_GIT
 
 else # HEADER_SAVE_SPEC
 
 # From a file
-HDRCK_SPEC:= cat $(HEADER_SPEC)
+HDRCK.SPEC:= cat $(HEADER_SPEC)
 
 # The file format can be overloaded in using the var HDRCK_EXTRA
-HDRCK_OPTS+= -spec-format 3-zeros
+HDRCK.OPTS+= -spec-format 3-zeros
 
 endif # HEADER_SAVE_SPEC
 endif # HEADER_SPEC
 
 ################################
-## Updates HDRCK_OPTS variable
+## Updates HDRCK.OPTS variable
 
 ifneq ($(HEADER_DISTRIB_FILE),)
 # Adds the option "-distrib-file"
-HDRCK_OPTS+= -distrib-file $(HEADER_DISTRIB_FILE)
+HDRCK.OPTS+= -distrib-file $(HEADER_DISTRIB_FILE)
 endif
 
 ifneq ($(HEADER_EXCEPTIONS),)
 # Adds the option "-header-except-file"
-HDRCK_OPTS+= -header-except-file $(HEADER_EXCEPTIONS)
+HDRCK.OPTS+= -header-except-file $(HEADER_EXCEPTIONS)
 endif
 
 ifneq ($(HEADER_REPO),)
 # Adds the option "-C"
-HDRCK_OPTS+= -C $(HEADER_REPO)
+HDRCK.OPTS+= -C $(HEADER_REPO)
 endif
 
 ifeq ($(HEADER_STRICT),yes)
 # Adds the option "-exit-on-warning"
-HDRCK_OPTS+= -exit-on-warning
+HDRCK.OPTS+= -exit-on-warning
 endif
 
 #####################################
 ## Identifies where are the headers
-## and updates HDRCK_OPTS variable
+## and updates HDRCK.OPTS variable
 
 ifeq ($(HEADER_OPEN_SOURCE),yes)
-HDRCK_OPTS+= $(addprefix -header-dirs=,$(addsuffix /open-source,$(HEADER_DIRS)))
+HDRCK.OPTS+= $(addprefix -header-dirs=,$(addsuffix /open-source,$(HEADER_DIRS)))
 else
 ifeq ($(HEADER_OPEN_SOURCE),no)
-HDRCK_OPTS+= $(addprefix -header-dirs=,$(addsuffix /close-source,$(HEADER_DIRS)))
+HDRCK.OPTS+= $(addprefix -header-dirs=,$(addsuffix /close-source,$(HEADER_DIRS)))
 else
 ifeq ($(HEADER_OPEN_SOURCE),)
-HDRCK_OPTS+= $(addprefix -header-dirs=,$(HEADER_DIRS))
+HDRCK.OPTS+= $(addprefix -header-dirs=,$(HEADER_DIRS))
 else
-HDRCK_OPTS+= $(addprefix -header-dirs=,$(addsuffix /$(HEADER_OPEN_SOURCE),$(HEADER_DIRS)))
+HDRCK.OPTS+= $(addprefix -header-dirs=,$(addsuffix /$(HEADER_OPEN_SOURCE),$(HEADER_DIRS)))
 endif
 endif
 endif
 
 #################################
 
-ifeq ($(HDRCK_SPEC),)
+ifeq ($(HDRCK.SPEC),)
 
 .PHONY: check-headers
 check-headers: $(FRAMAC_HDRCK)
@@ -192,22 +204,103 @@ headers: $(FRAMAC_HDRCK)
 	$(error "Please set HEADER_SPEC variable to a file containing the header specification.")
 else
 
+ifneq ($(HDRCK.HAS_GIT),)
+
+define HDRCK.file-list-from-git-diff
+$(GIT) diff --name-status $(1) | $(GREP) -v "^D" | $(SED) "s/^.[ \t]*//" | $(TR) '\n' '\000' | $(HDRCK.FILE_ATTR)
+endef
+
+HDRCK.main-targets=check-headers headers
+define HDRCK.file-list-filter-with-git-diff
+HDRCK.$(1)-filter-targets=$$(addsuffix .$(1),$$(HDRCK.main-targets))
+.PHONY: $(LINT.$(1)-filter-targets)
+$$(HDRCK.$(1)-filter-targets):: HDRCK.SPEC=$$(call HDRCK.file-list-from-git-diff,$(2))
+$$(HDRCK.$(1)-filter-targets):: %.$(1) : $(3) %
+	@echo [HDRCK] Done: HDRCK_DIFF=\"$(2)\" make $$(basename $$@)
+	@echo [HDRCK] checked file list:
+	$$(GIT) diff --name-status $(2)
+endef
+
+ifneq ($(HEADER_DIFF),)
+
+$(info [HDRCK] Looking at files modified from branch/commit: '$(HEADER_DIFF)')
+HDRCK.SPEC=$(call LINT.file-list-from-git-diff,$(HEADER_DIFF))
+$(info $(HEADER.FILE_LIST))
+
+endif # $(HEADER_DIFF)
+
+#### rules for make <headers-target>.before-push
+##   looks at files modified from origin/$(git branch --show-current) and checks that there is no staged nor unstaged files
+
+PHONY: HDRCK.checked-unmodified-ok
+HDRCK.checked-unmodified-ok:
+	$(eval HDRCK.checked-unmodified := $(shell $(GIT) diff --name-status HEAD | $(WC) -l))
+	if [ 0 != $(HDRCK.checked-unmodified) ]; then \
+           echo "[HDRCK] Staged or unstaged files=$(HDRCK.checked-unmodified):"; \
+            $(GIT) diff --name-status HEAD; \
+           echo "[HDRCK] Error: may check some staged or unstaged file versions" ; \
+           exit 1; \
+        fi;
+
+$(eval $(call HDRCK.file-list-filter-with-git-diff,before-push,--cached origin/$(shell git branch --show-current),HDRCK.checked-unmodified-ok))
+
+#### rules for make <headers-target>.unstaged
+##   looks at unstaged files
+
+$(eval $(call HDRCK.file-list-filter-with-git-diff,unstaged, ))
+
+#### rules for make <headers-target>.before-commit
+##   looks at staged files and checks that there is no unstaged files
+
+PHONY: HDRCK.checked-unstaged-ok
+HDRCK.checked-unstaged-ok:
+	$(eval HDRCK.checked-unstaged := $(shell $(GIT) diff --name-status | $(WC) -l))
+	if [ 0 != $(HDRCK.checked-unstaged) ]; then \
+	   echo "[HDRCK] Unstaged files=$(HDRCK.checked-unstaged):"; \
+           $(GIT) diff --name-status ; \
+           echo "[HDRCK] Error: may check some unstaged version files version." ; \
+           exit 1; \
+        fi;
+
+$(eval $(call HDRCK.file-list-filter-with-git-diff,before-commit,--cached HEAD,HDRCK.checked-unstaged-ok))
+
+#### rules for make <headers-target>.before-commit-a
+## looks at unstaged and staged files
+
+$(eval $(call HDRCK.file-list-filter-with-git-diff,before-commit-a,HEAD,))
+
+#### rules for make <headers-target>.before-commit-a--ammend
+##   looks at unstaged, staged and previously committed files
+
+$(eval $(call HDRCK.file-list-filter-with-git-diff,before-commit-a--ammend,HEAD~1,))
+
+#### rules for make <headers-target>.before-commit--amend
+##   looks at staged and previously committed files and checks that there is no unstaged files
+
+$(eval $(call HDRCK.file-list-filter-with-git-diff,before-commit--ammend,HEAD~1,HDRCK.checked-unstaged-ok))
+
+#### rules for make <headers-target>.previous-commit
+## looks at files of the last commit and checks that there is no staged nor unstaged files
+
+$(eval $(call HDRCK.file-list-filter-with-git-diff,previous-commit,HEAD~1,HDRCK.checked-unmodified-ok))
+
+endif # $(HDRCK.HAS_GIT)
+
 .PHONY: check-headers
 check-headers: $(FRAMAC_HDRCK)
-	$(HDRCK_SPEC) | $(HDRCK) $(HDRCK_OPTS) $(HDRCK_EXTRA)
+	$(HDRCK.SPEC) | $(HDRCK.CMD) $(HDRCK.OPTS) $(HDRCK_EXTRA)
 
 .PHONY: headers
 headers: $(FRAMAC_HDRCK)
-	$(HDRCK_SPEC) | $(HDRCK) -update $(HDRCK_OPTS) $(HDRCK_EXTRA)
+	$(HDRCK.SPEC) | $(HDRCK.CMD) -update $(HDRCK.OPTS) $(HDRCK_EXTRA)
 
-endif # $(HDRCK_SPEC)
+endif # $(HDRCK.SPEC)
 
 #################################
 
 .PHONY: headers.info
 headers.info:
 	echo "FRAMAC_HDRCK='$(FRAMAC_HDRCK)'"
-	echo "HEADER_HAS_GIT='$(HEADER_HAS_GIT)'"
 	echo "HEADER_OPEN_SOURCE='$(HEADER_OPEN_SOURCE)'"
 	echo "HEADER_STRICT='$(HEADER_STRICT)'"
 	echo "HEADER_DIRS='$(HEADER_STRICT)'"
@@ -215,9 +308,10 @@ headers.info:
 	echo "HEADER_EXCEPTIONS='$(HEADER_EXCEPTIONS)'"
 	echo "HEADER_REPO='$(HEADER_REPO)'"
 	echo "HEADER_SPEC='$(HEADER_SPEC)'"
-	echo "HDRCK='$(HDRCK)'"
-	echo "HDRCK_SPEC='$(HDRCK_SPEC)'"
-	echo "HDRCK_OPTS='$(HDRCK_OPTS)'"
+	echo "HDRCK.HAS_GIT='$(HDRCK.HAS_GIT)'"
+	echo "HDRCK.CMD='$(HDRCK.CMD)'"
+	echo "HDRCK.SPEC='$(HDRCK.SPEC)'"
+	echo "HDRCK.OPTS='$(HDRCK.OPTS)'"
 
 
 ###############################################################################
diff --git a/share/Makefile.linting b/share/Makefile.linting
index 922fa4b162c729b3d8c9cfac6394cdf6d9fe384b..afaf8e870e5e65b0d3f9494bcaa5e3b7d153d452 100644
--- a/share/Makefile.linting
+++ b/share/Makefile.linting
@@ -217,8 +217,8 @@ LINT.$(1)-filter-targets=$$(addsuffix .$(1),$$(LINT.main-targets))
 $$(LINT.$(1)-filter-targets):: LINT.FILE_LIST=$$(call LINT.file-list-from-git-diff,$(2))
 $$(LINT.$(1)-filter-targets):: %.$(1) : $(3) %
 	@echo [LINT] Done: LINT_DIFF=\"$(2)\" make $$(basename $$@)
-	@echo [LINT] git diff --name-status
-	$$(GIT) diff --name-status HEAD
+	@echo [LINT] checked file list:
+	$$(GIT) diff --name-status $(2)
 endef
 
 ifeq ($(LINT_DIFF),)
@@ -262,7 +262,7 @@ LINT.checked-unstaged-ok:
            exit 1; \
         fi;
 
-$(eval $(call LINT.file-list-filter-with-git-diff,staged,--cached HEAD,LINT.checked-unstaged-ok))
+$(eval $(call LINT.file-list-filter-with-git-diff,before-commit,--cached HEAD,LINT.checked-unstaged-ok))
 
 #### rules for make <lint-target>.before-commit-a
 ## looks at unstaged and staged files