diff options
| author | Matthieu Sozeau | 2014-07-03 18:51:13 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-07-03 18:53:17 +0200 |
| commit | e7ba2a9be24823503495e959f0dffc131e99801b (patch) | |
| tree | db0a3979974c88e101804438cfb89c1ddc70742d /pretyping/evarconv.ml | |
| parent | f2327aa3c69f1695f99e2ccbfe00c4e54e56e7d2 (diff) | |
Fix eta expansion of primitive records (HoTT bug #78), which now fails cleanly when called
on partially applied constructors. Also protect evar_conv from that case.
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index e9d152de2d..cef8215866 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -708,7 +708,9 @@ and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = exact_ise_stack2 env evd (evar_conv_x ts) l1' (Stack.append_app_list l2' Stack.empty) else raise (Failure "") - with Failure _ -> UnifFailure(evd,NotSameHead)) + with + | Invalid_argument _ (* Stack.tail: partially applied constructor *) + | Failure _ -> UnifFailure(evd,NotSameHead)) | _ -> UnifFailure (evd,NotSameHead) (* Profiling *) |