diff options
| -rw-r--r-- | dev/include | 1 | ||||
| -rw-r--r-- | dev/top_printers.ml | 4 | ||||
| -rw-r--r-- | pretyping/unification.ml | 22 | ||||
| -rw-r--r-- | pretyping/unification.mli | 9 |
4 files changed, 28 insertions, 8 deletions
diff --git a/dev/include b/dev/include index 5d4872273..705e8e375 100644 --- a/dev/include +++ b/dev/include @@ -28,6 +28,7 @@ #install_printer (* Goal.goal *) ppgoalgoal;; #install_printer (* metaset.t *) ppmetas;; #install_printer (* evar_map *) ppevm;; +#install_printer (* ExistentialSet.t *) ppexistentialset;; #install_printer (* clenv *) ppclenv;; #install_printer (* env *) ppenv;; diff --git a/dev/top_printers.ml b/dev/top_printers.ml index bb8d0a68b..278fdb399 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -114,6 +114,10 @@ let pp_transparent_state s = pp (pr_transparent_state s) let ppmetas metas = pp(pr_metaset metas) let ppevm evd = pp(pr_evar_map (Some 2) evd) let ppevmall evd = pp(pr_evar_map None evd) +let pr_existentialset evars = + prlist_with_sep spc pr_meta (ExistentialSet.elements evars) +let ppexistentialset evars = + pp (pr_existentialset evars) let ppclenv clenv = pp(pr_clenv clenv) let ppgoalgoal gl = pp(Goal.pr_goal gl) let ppgoal g = pp(Printer.pr_goal g) 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) diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 37eaa5802..cc781c871 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -66,3 +66,12 @@ val w_merge : env -> bool -> unify_flags -> evar_map * (metavariable * constr * (instance_constraint * instance_typing_status)) list * (env * types pexistential * types) list -> evar_map +val unify_0 : Environ.env -> + Evd.evar_map -> + Evd.conv_pb -> + unify_flags -> + Term.types -> + Term.types -> + Evd.evar_map * Evd.metabinding list * + (Environ.env * Term.types Term.pexistential * Term.constr) list + |