From 27b6f605efb2e94656c3405ddc271a775fbdab7e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 8 Jun 2019 21:46:56 +0200
Subject: Fix #10339: Anomaly in Ltac2.

We use a user-facing wrapper instead of a low-level function raising internal
exceptions.
---
 user-contrib/Ltac2/tac2intern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/user-contrib/Ltac2/tac2intern.ml b/user-contrib/Ltac2/tac2intern.ml
index de99fb167f..76556430df 100644
--- a/user-contrib/Ltac2/tac2intern.ml
+++ b/user-contrib/Ltac2/tac2intern.ml
@@ -367,7 +367,7 @@ let unify_arrow ?loc env ft args =
     iter ft args true
   | GTypVar id, (_, t) :: args ->
     let ft = GTypVar (fresh_id env) in
-    let () = unify_var env id (GTypArrow (t, ft)) in
+    let () = unify ?loc env (GTypVar id) (GTypArrow (t, ft)) in
     iter ft args true
   | GTypRef _, _ :: _ ->
     if is_fun then
-- 
cgit v1.2.3