diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarsolve.ml | 27 | ||||
| -rw-r--r-- | pretyping/evd.ml | 5 | ||||
| -rw-r--r-- | pretyping/evd.mli | 6 |
3 files changed, 24 insertions, 14 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 940eebbf7e..a6d5e1eac1 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1132,35 +1132,34 @@ let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,ar if force then ensure_evar_independent g env evd ev1 ev2, None else (evd,ev1,ev2),pbty in let evi = Evd.find evd evk1 in + let evd = try (* ?X : Π Δ. Type i = ?Y : Π Δ'. Type j. The body of ?X and ?Y just has to be of type Π Δ. Type k for some k <= i, j. *) let evienv = Evd.evar_env evi in - let ctx, i = Reduction.dest_arity evienv evi.evar_concl in + let ctx1, i = Reduction.dest_arity evienv evi.evar_concl in let evi2 = Evd.find evd evk2 in let evi2env = Evd.evar_env evi2 in - let ctx', j = Reduction.dest_arity evi2env evi2.evar_concl in + let ctx2, j = Reduction.dest_arity evi2env evi2.evar_concl in let ui, uj = univ_of_sort i, univ_of_sort j in if i == j || Evd.check_eq evd ui uj then (* Shortcut, i = j *) - solve_evar_evar_aux f g env evd pbty ev1 ev2 - (* Avoid looping if postponing happened on previous evar/evar problem *) + evd else if Evd.check_leq evd ui uj then - solve_evar_evar_aux f g env evd (opp_problem pbty) ev2 ev1 + let t2 = it_mkProd_or_LetIn (mkSort i) ctx2 in + downcast evk2 t2 evd else if Evd.check_leq evd uj ui then - solve_evar_evar_aux f g env evd pbty ev1 ev2 + let t1 = it_mkProd_or_LetIn (mkSort j) ctx1 in + downcast evk1 t1 evd else let evd, k = Evd.new_sort_variable univ_flexible_alg evd in - let evd, ev3 = - Evarutil.new_pure_evar (Evd.evar_hyps evi) evd - ~src:evi.evar_source ~filter:evi.evar_filter - ?candidates:evi.evar_candidates (it_mkProd_or_LetIn (mkSort k) ctx) - in + let t1 = it_mkProd_or_LetIn (mkSort k) ctx1 in + let t2 = it_mkProd_or_LetIn (mkSort k) ctx2 in let evd = Evd.set_leq_sort env (Evd.set_leq_sort env evd k i) k j in - let evd = solve_evar_evar_aux f g env evd (opp_problem pbty) (ev3,args1) ev1 in - f env evd (opp_problem pbty) ev2 (whd_evar evd (mkEvar (ev3,args1))) + downcast evk2 t2 (downcast evk1 t1 evd) with Reduction.NotArity -> - solve_evar_evar_aux f g env evd pbty ev1 ev2 + evd in + solve_evar_evar_aux f g env evd pbty ev1 ev2 type conv_fun = env -> evar_map -> conv_pb -> constr -> constr -> unification_result diff --git a/pretyping/evd.ml b/pretyping/evd.ml index d5e3c6715c..9336841436 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -853,6 +853,11 @@ let restrict evk evk' filter ?candidates evd = { evd with undf_evars = EvMap.add evk' evar_info' undf_evars; defn_evars; evar_names } +let downcast evk ccl evd = + let evar_info = EvMap.find evk evd.undf_evars in + let evar_info' = { evar_info with evar_concl = ccl } in + { evd with undf_evars = EvMap.add evk evar_info' evd.undf_evars } + (* extracts conversion problems that satisfy predicate p *) (* Note: conv_pbs not satisying p are stored back in reverse order *) let extract_conv_pbs evd p = diff --git a/pretyping/evd.mli b/pretyping/evd.mli index df5269d345..f800a45474 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -243,6 +243,12 @@ val evar_declare : val restrict : evar -> evar -> Filter.t -> ?candidates:constr list -> evar_map -> evar_map +(** Restrict an undefined evar into a new evar by filtering context and + possibly limiting the instances to a set of candidates *) + +val downcast : evar -> types -> evar_map -> evar_map +(** Change the type of an undefined evar to a new type assumed to be a + subtype of its current type; subtyping must be ensured by caller *) val evar_source : existential_key -> evar_map -> Evar_kinds.t located (** Convenience function. Wrapper around {!find} to recover the source of an |