diff --git a/.github/workflows/docker-ci.yml b/.github/workflows/docker-action.yml
similarity index 100%
rename from .github/workflows/docker-ci.yml
rename to .github/workflows/docker-action.yml
diff --git a/.github/workflows/nix-action.yml b/.github/workflows/nix-action.yml
new file mode 100644
index 0000000..0bdf051
--- /dev/null
+++ b/.github/workflows/nix-action.yml
@@ -0,0 +1,52 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+name: Nix CI
+
+on:
+  push:
+    branches:
+      - v8.13
+  pull_request:
+    paths:
+    - .github/workflows/**
+  pull_request_target:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        overrides:
+          - 'coq = "8.13"'
+      fail-fast: false
+    steps:
+      - name: Determine which ref to test
+        run: |
+          if [[ ${{ github.event_name }} =~ "pull_request" ]]; then
+            merge_commit=$(git ls-remote ${{ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge | cut -f1)
+            if [ -z "$merge_commit" ]; then
+              echo "tested_ref=refs/pull/${{ github.event.number }}/head" >> $GITHUB_ENV
+            else
+              echo "tested_ref=refs/pull/${{ github.event.number }}/merge" >> $GITHUB_ENV
+            fi
+          else
+            echo "tested_ref=${{ github.ref }}" >> $GITHUB_ENV
+          fi
+      - uses: cachix/install-nix-action@v12
+        with:
+          nix_path: nixpkgs=channel:nixpkgs-unstable
+      - uses: cachix/cachix-action@v8
+        with:
+          name: coq
+      - uses: cachix/cachix-action@v8
+        with:
+          name: coq-community
+          authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
+      - uses: cachix/cachix-action@v8
+        with:
+          name: math-comp
+      - uses: actions/checkout@v2
+        with:
+          ref: ${{ env.tested_ref }}
+      - run: >
+          nix-build https://coq.inria.fr/nix/toolbox --argstr job aac-tactics --arg override '{ ${{ matrix.overrides }}; aac-tactics = builtins.filterSource (path: _: baseNameOf path != ".git") ./.; }'
diff --git a/.github/workflows/nix-ci.yml b/.github/workflows/nix-ci.yml
deleted file mode 100644
index 4283eee..0000000
--- a/.github/workflows/nix-ci.yml
+++ /dev/null
@@ -1,30 +0,0 @@
-# This file was generated from `meta.yml`, please do not edit manually.
-# Follow the instructions on https://github.com/coq-community/templates to regenerate.
-name: Nix CI
-
-on:
-  push:
-    branches:
-      - v8.13
-  pull_request:
-    branches:
-      - '**'
-
-jobs:
-  build:
-    runs-on: ubuntu-latest
-    strategy:
-      matrix:
-        version_or_url:
-          - 'https://github.com/coq/coq-on-cachix/tarball/v8.13'
-      fail-fast: false
-    steps:
-      - uses: cachix/install-nix-action@v12
-        with:
-          nix_path: nixpkgs=channel:nixpkgs-unstable
-      - uses: cachix/cachix-action@v8
-        with:
-          # Name of a cachix cache to pull/substitute
-          name: coq
-      - uses: actions/checkout@v2
-      - run: nix-build --argstr coq-version-or-url "${{ matrix.version_or_url }}"
diff --git a/meta.yml b/meta.yml
index 3e7956a..b4050b2 100644
--- a/meta.yml
+++ b/meta.yml
@@ -55,7 +55,7 @@ supported_ocaml_versions:
     opam: '{>= "4.05.0"}'
 
 tested_coq_nix_versions:
-- version_or_url: https://github.com/coq/coq-on-cachix/tarball/v8.13
+- coq_version: '8.13'
 
 tested_coq_opam_versions:
 - version: '8.13'
diff --git a/src/aac_rewrite.ml b/src/aac_rewrite.ml
index 6096ad2..cab499c 100644
--- a/src/aac_rewrite.ml
+++ b/src/aac_rewrite.ml
@@ -346,7 +346,7 @@ let aac_rewrite_wrap  ?abort ?(l2r=true) ?(show = false) ?(in_left=true) ?strict
       let check_type x =
         Tacmach.New.pf_conv_x goal x rlt.Coq.Relation.carrier
       in
-      let hypinfo = Coq.Rewrite.get_hypinfo env sigma rew ~l2r ?check_type:(Some check_type) in      
+      let hypinfo = Coq.Rewrite.get_hypinfo env sigma ?check_type:(Some check_type) rew ~l2r in
       let sigma,rewinfo = dispatch env sigma in_left concl hypinfo in
       let sigma =
         match extra with
diff --git a/src/coq.ml b/src/coq.ml
index 27a0189..9dd9a01 100644
--- a/src/coq.ml
+++ b/src/coq.ml
@@ -352,7 +352,7 @@ type hypinfo =
       l2r : bool; 			(** rewriting from left to right  *)
     }
 
-let get_hypinfo env sigma c ?check_type ~l2r  : hypinfo =
+let get_hypinfo env sigma ?check_type c ~l2r : hypinfo =
   let ctype = Typing.unsafe_type_of env sigma c in
   let (rel_context, body_type) = decompose_prod_assum sigma ctype in
   let rec check f e =
diff --git a/src/coq.mli b/src/coq.mli
index 2f06fd1..d1e9628 100644
--- a/src/coq.mli
+++ b/src/coq.mli
@@ -174,11 +174,11 @@ type hypinfo =
       l2r : bool; 			(** rewriting from left to right  *)
     }
 
-(** [get_hypinfo H ?check_type l2r] analyse the hypothesis H, and
+(** [get_hypinfo ?check_type H l2r] analyse the hypothesis H, and
     build the related hypinfo. Moreover, an optionnal
     function can be provided to check the type of every free
     variable of the body of the hypothesis.  *)
-val get_hypinfo : Environ.env -> Evd.evar_map ->  EConstr.constr -> ?check_type:(EConstr.types -> bool) -> l2r:bool -> hypinfo
+val get_hypinfo : Environ.env -> Evd.evar_map -> ?check_type:(EConstr.types -> bool) -> EConstr.constr -> l2r:bool -> hypinfo
  
 (** {2 Rewriting with bindings}