diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-08-08 16:11:23 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-08-09 21:31:37 +0200 |
| commit | b3d64ad3164517ee0eeb148c2f1d6c44eb9cf23d (patch) | |
| tree | 34db6dc74629c9e260a3da1d6dfbe352203b408c | |
| parent | 3491563fae26168f8b06b8beb81be5427c3f4c8c (diff) | |
Do early occur-check in unification to allow eta to fire (fixes bug #3477)
| -rw-r--r-- | pretyping/unification.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index df669f5be..a864ccc46 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -509,13 +509,15 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag evarsubst) else error_cannot_unify_local curenv sigma (m,n,cM) | Evar (evk,_ as ev), _ - when not (Evar.Set.mem evk flags.frozen_evars) -> + when not (Evar.Set.mem evk flags.frozen_evars) + && not (occur_evar evk cN) -> let cmvars = free_rels cM and cnvars = free_rels cN in if Int.Set.subset cnvars cmvars then sigma,metasubst,((curenv,ev,cN)::evarsubst) else error_cannot_unify_local curenv sigma (m,n,cN) | _, Evar (evk,_ as ev) - when not (Evar.Set.mem evk flags.frozen_evars) -> + when not (Evar.Set.mem evk flags.frozen_evars) + && not (occur_evar evk cM) -> let cmvars = free_rels cM and cnvars = free_rels cN in if Int.Set.subset cmvars cnvars then sigma,metasubst,((curenv,ev,cM)::evarsubst) @@ -546,8 +548,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag | _, Lambda (na,t2,c2) when flags.modulo_eta -> unirec_rec (push (na,t2) curenvnb) CONV true wt substn (mkApp (lift 1 cM,[|mkRel 1|])) c2 - - (* TODO: eta for records *) + (* For records, eta-expansion is done through unify_app -> expand -> infer_conv *) | Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) -> (try |