diff options
| author | Emilio Jesus Gallego Arias | 2019-06-16 14:50:38 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-16 14:50:38 +0200 |
| commit | 6eba5b5ba91f9ec02b809e0c223324e0f4fdbf85 (patch) | |
| tree | 3914740835572b424500576e11fe6e4e1fac1ba4 | |
| parent | 5d58496c27fc5767c7841734c0f01a739cf529ab (diff) | |
| parent | 27b6f605efb2e94656c3405ddc271a775fbdab7e (diff) | |
Merge PR #10345: Fix #10339: Anomaly in Ltac2.
Reviewed-by: ejgallego
| -rw-r--r-- | user-contrib/Ltac2/tac2intern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |