diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarsolve.ml | 5 | ||||
| -rw-r--r-- | pretyping/unification.ml | 15 | ||||
| -rw-r--r-- | pretyping/unification.mli | 2 |
3 files changed, 12 insertions, 10 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 715b80f428..c58ebe1bbd 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -810,7 +810,8 @@ let check_evar_instance unify flags env evd evk1 body = (* This happens in practice, cf MathClasses build failure on 2013-3-15 *) let ty = try Retyping.get_type_of ~lax:true evenv evd body - with Retyping.RetypeError _ -> user_err (Pp.(str "Ill-typed evar instance")) + with Retyping.RetypeError _ -> + let loc, _ = evi.evar_source in user_err ?loc (Pp.(str "Ill-typed evar instance")) in match unify flags TypeUnification evenv evd Reduction.CUMUL ty evi.evar_concl with | Success evd -> evd @@ -1575,7 +1576,7 @@ let rec invert_definition unify flags choose imitate_defs match EConstr.kind !evdref t with | Rel i when i>k -> let open Context.Rel.Declaration in - (match Environ.lookup_rel (i-k) env' with + (match Environ.lookup_rel i env' with | LocalAssum _ -> project_variable (RelAlias (i-k)) | LocalDef (_,b,_) -> try project_variable (RelAlias (i-k)) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 982814fdfc..c352a6ac1f 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -38,7 +38,7 @@ type metabinding = (metavariable * EConstr.constr * (instance_constraint * insta type subst0 = (evar_map * metabinding list * - (Environ.env * EConstr.existential * EConstr.t) list) + ((Environ.env * int) * EConstr.existential * EConstr.t) list) module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration @@ -227,7 +227,7 @@ let solve_pattern_eqn_array (env,nb) f l c (sigma,metasubst,evarsubst : subst0) | Evar ev -> let env' = pop_rel_context nb env in let sigma,c = pose_all_metas_as_evars env' sigma c in - sigma,metasubst,(env,ev,solve_pattern_eqn env sigma l c)::evarsubst + sigma,metasubst,((env,nb),ev,solve_pattern_eqn env sigma l c)::evarsubst | _ -> assert false let push d (env,n) = (push_rel_assum d env,n+1) @@ -769,21 +769,21 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e | Some sigma -> sigma, metasubst, evarsubst | None -> - sigma,metasubst,((curenv,ev,cN)::evarsubst) + sigma,metasubst,((curenvnb,ev,cN)::evarsubst) end | Evar (evk,_ as ev), _ when is_evar_allowed flags evk && not (occur_evar sigma evk cN) -> let cmvars = free_rels sigma cM and cnvars = free_rels sigma cN in if Int.Set.subset cnvars cmvars then - sigma,metasubst,((curenv,ev,cN)::evarsubst) + sigma,metasubst,((curenvnb,ev,cN)::evarsubst) else error_cannot_unify_local curenv sigma (m,n,cN) | _, Evar (evk,_ as ev) when is_evar_allowed flags evk && not (occur_evar sigma evk cM) -> let cmvars = free_rels sigma cM and cnvars = free_rels sigma cN in if Int.Set.subset cmvars cnvars then - sigma,metasubst,((curenv,ev,cM)::evarsubst) + sigma,metasubst,((curenvnb,ev,cM)::evarsubst) else error_cannot_unify_local curenv sigma (m,n,cN) | Sort s1, Sort s2 -> (try @@ -1357,7 +1357,7 @@ let w_merge env with_types flags (evd,metas,evars : subst0) = (* Process evars *) match evars with - | (curenv,(evk,_ as ev),rhs)::evars' -> + | ((curenv,nb),(evk,_ as ev),rhs)::evars' -> if Evd.is_defined evd evk then let v = mkEvar ev in let (evd,metas',evars'') = @@ -1376,7 +1376,8 @@ let w_merge env with_types flags (evd,metas,evars : subst0) = w_merge_rec evd' metas evars eqns else let evd' = - let evd', rhs'' = pose_all_metas_as_evars curenv evd rhs' in + let env' = pop_rel_context nb curenv in + let evd', rhs'' = pose_all_metas_as_evars env' evd rhs' in try solve_simple_evar_eqn eflags curenv evd' ev rhs'' with Retyping.RetypeError _ -> error_cannot_unify curenv evd' (mkEvar ev,rhs'') diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 5462e09359..077597c278 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -105,7 +105,7 @@ type metabinding = (metavariable * constr * (instance_constraint * instance_typi type subst0 = (evar_map * metabinding list * - (Environ.env * existential * t) list) + ((Environ.env * int) * existential * t) list) val w_merge : env -> bool -> core_unify_flags -> subst0 -> evar_map |