diff options
| author | Pierre-Marie Pédrot | 2019-06-08 21:46:56 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-08 21:46:56 +0200 |
| commit | 27b6f605efb2e94656c3405ddc271a775fbdab7e (patch) | |
| tree | f01870646eaa3803ef96531fc2f1d6c04f5c5dfa | |
| parent | 65f75de6929530252a3235af54a0da56980fa02d (diff) | |
Fix #10339: Anomaly in Ltac2.
We use a user-facing wrapper instead of a low-level function raising internal
exceptions.
| -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 |