diff options
Diffstat (limited to 'pretyping/evarutil.ml')
| -rw-r--r-- | pretyping/evarutil.ml | 37 |
1 files changed, 30 insertions, 7 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 201a16eb..b27803bd 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -525,7 +525,7 @@ let rec check_and_clear_in_constr env evdref err ids c = let clear_hyps_in_evi_main env evdref hyps terms ids = (* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some hypothesis does not depend on a element of ids, and erases ids in - the contexts of the evars occuring in evi *) + the contexts of the evars occurring in evi *) let terms = List.map (check_and_clear_in_constr env evdref (OccurHypInSimpleClause None) ids) terms in let nhyps = @@ -713,9 +713,10 @@ let define_pure_evar_as_product evd evk = let evi = Evd.find_undefined evd evk in let evenv = evar_env evi in let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in - let concl = whd_evar evd evi.evar_concl in + let concl = whd_betadeltaiota evenv evd evi.evar_concl in let s = destSort concl in - let evd1,(dom,u1) = new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in + let evd1,(dom,u1) = + new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in let evd2,rng = let newenv = push_named (id, None, dom) evenv in let src = evar_source evk evd1 in @@ -724,8 +725,9 @@ let define_pure_evar_as_product evd evk = (* Impredicative product, conclusion must fall in [Prop]. *) new_evar newenv evd1 concl ~src ~filter else + let status = univ_flexible_alg in let evd3, (rng, srng) = - new_type_evar newenv evd1 univ_flexible_alg ~src ~filter in + new_type_evar newenv evd1 status ~src ~filter in let prods = Univ.sup (univ_of_sort u1) (univ_of_sort srng) in let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) s in evd3, rng @@ -757,7 +759,7 @@ let define_evar_as_product evd (evk,args) = let define_pure_evar_as_lambda env evd evk = let evi = Evd.find_undefined evd evk in let evenv = evar_env evi in - let typ = whd_betadeltaiota env evd (evar_concl evi) in + let typ = whd_betadeltaiota evenv evd (evar_concl evi) in let evd1,(na,dom,rng) = match kind_of_term typ with | Prod (na,dom,rng) -> (evd,(na,dom,rng)) | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd typ @@ -795,8 +797,10 @@ let define_evar_as_sort env evd (ev,args) = let evd, u = new_univ_variable univ_rigid evd in let evi = Evd.find_undefined evd ev in let s = Type u in + let concl = whd_betadeltaiota (evar_env evi) evd evi.evar_concl in + let sort = destSort concl in let evd' = Evd.define ev (mkSort s) evd in - Evd.set_leq_sort env evd' (Type (Univ.super u)) (destSort evi.evar_concl), s + Evd.set_leq_sort env evd' (Type (Univ.super u)) sort, s (* We don't try to guess in which sort the type should be defined, since any type has type Type. May cause some trouble, but not so far... *) @@ -844,6 +848,25 @@ let subterm_source evk (loc,k) = (loc,Evar_kinds.SubEvar evk) -(** Term exploration up to isntantiation. *) +(** Term exploration up to instantiation. *) let kind_of_term_upto sigma t = Constr.kind (Reductionops.whd_evar sigma t) + +(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and + [u] up to existential variable instantiation and equalisable + universes. The term [t] is interpreted in [sigma1] while [u] is + interpreted in [sigma2]. The universe constraints in [sigma2] are + assumed to be an extention of those in [sigma1]. *) +let eq_constr_univs_test sigma1 sigma2 t u = + (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *) + let open Evd in + let b, c = + Universes.eq_constr_univs_infer_with + (fun t -> kind_of_term_upto sigma1 t) + (fun u -> kind_of_term_upto sigma2 u) + (universes sigma2) t u + in + if b then + try let _ = add_universe_constraints sigma2 c in true + with Univ.UniverseInconsistency _ | UniversesDiffer -> false + else false |