diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-08-04 14:42:55 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-08-04 14:42:55 +0000 |
| commit | 726130d3d847e59d3556f6b302de155dc052d6a4 (patch) | |
| tree | 1a867c16ecfb46992dfc1ee76f7f1cb0b152249f /pretyping/unification.ml | |
| parent | cd411cddcd2f24c892146916e530635dda086d8d (diff) | |
Fix unification: detect invalid evar instantiations due to scoping earlier.
Add a debug printer for existential sets (used for frozen_evars in w_unify).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14384 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 22 |
1 files changed, 14 insertions, 8 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 0d2b2af00..31bf431da 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -327,9 +327,10 @@ let oracle_order env cf1 cf2 = | None -> Some true | Some k2 -> Some (Conv_oracle.oracle_order k1 k2) -let do_reduce ts env sigma c = - let (t, l) = whd_betaiota_deltazeta_for_iota_state ts env sigma (c, empty_stack) in - applist (t, list_of_stack l) +let do_reduce ts (env, nb) sigma c = + let (t, stack') = whd_betaiota_deltazeta_for_iota_state ts env sigma (c, empty_stack) in + let l = list_of_stack stack' in + applist (t, l) let use_full_betaiota flags = flags.modulo_betaiota && Flags.version_strictly_greater Flags.V8_3 @@ -369,11 +370,16 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag else error_cannot_unify_local curenv sigma (m,n,cM) | Evar (evk,_ as ev), _ when not (ExistentialSet.mem evk flags.frozen_evars) -> - sigma,metasubst,((curenv, ev,cN)::evarsubst) + let cmvars = free_rels cM and cnvars = free_rels cN in + if Intset.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 (ExistentialSet.mem evk flags.frozen_evars) -> - sigma,metasubst,((curenv, ev,cM)::evarsubst) - + let cmvars = free_rels cM and cnvars = free_rels cN in + if Intset.subset cmvars cnvars then + sigma,metasubst,((curenv,ev,cM)::evarsubst) + else error_cannot_unify_local curenv sigma (m,n,cN) | Sort s1, Sort s2 -> (try let sigma' = @@ -457,11 +463,11 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag and reduce curenvnb pb b (sigma, metas, evars as substn) cM cN = if use_full_betaiota flags && not (subterm_restriction b flags) then - let cM' = do_reduce flags.modulo_delta (fst curenvnb) sigma cM in + let cM' = do_reduce flags.modulo_delta curenvnb sigma cM in if not (eq_constr cM cM') then unirec_rec curenvnb pb b substn cM' cN else - let cN' = do_reduce flags.modulo_delta (fst curenvnb) sigma cN in + let cN' = do_reduce flags.modulo_delta curenvnb sigma cN in if not (eq_constr cN cN') then unirec_rec curenvnb pb b substn cM cN' else error_cannot_unify (fst curenvnb) sigma (cM,cN) |