diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-06-13 16:37:29 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-06-13 17:08:13 +0200 |
| commit | bb43103f7ecea16e634d448215f24d6d55d56eb1 (patch) | |
| tree | 7de6b19bfc24428b90a48323e0d36c837df34ce4 | |
| parent | 87be9070b3415f31027b78165b213de34c168043 (diff) | |
evar_conv: Refine occur_rigidly
This avoids postponing constraints which will surely produce
an occur-check and allow to backtrack on first-order unifications
producing those constraints directly (e.g. to apply eta).
(fixes HoTT/HoTT with 8.5).
| -rw-r--r-- | pretyping/evarconv.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 96c90e2fc..aead1cb35 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -97,8 +97,7 @@ let position_problem l2r = function | CUMUL -> Some l2r let occur_rigidly ev evd t = - let (l, app) = decompose_app_vect t in - let rec aux t = + let rec aux t = match kind_of_term (whd_evar evd t) with | App (f, c) -> if aux f then Array.exists aux c else false | Construct _ | Ind _ | Sort _ | Meta _ | Fix _ | CoFix _ -> true @@ -110,7 +109,7 @@ let occur_rigidly ev evd t = | Prod (_, b, t) -> ignore(aux b || aux t); true | Rel _ | Var _ -> false | Case _ -> false - in Array.exists (fun t -> try ignore(aux t); false with Occur -> true) app + in try ignore(aux t); false with Occur -> true (* [check_conv_record env sigma (t1,stack1) (t2,stack2)] tries to decompose the problem (t1 stack1) = (t2 stack2) into a problem |