diff options
| -rw-r--r-- | pretyping/evd.ml | 17 | ||||
| -rw-r--r-- | pretyping/evd.mli | 1 | ||||
| -rw-r--r-- | pretyping/unification.ml | 8 |
3 files changed, 16 insertions, 10 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 3c87defa0c..ecad02cd40 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -190,15 +190,15 @@ let rec canonical_find u scstr = let find_univ u scstr = try canonical_find u scstr with Not_found -> u, DefinedSort (Type u) - + let whd_sort_var scstr t = match kind_of_term t with Sort(Type u) -> (try match canonical_find u scstr with - _, DefinedSort s -> mkSort s - | _ -> t - with Not_found -> t) + | _, DefinedSort s -> mkSort s + | _ -> t + with Not_found -> t) | _ -> t let rec set_impredicative u s scstr = @@ -533,6 +533,7 @@ let empty = { let evars_reset_evd evd d = {d with evars = (fst evd.evars, EvarMap.merge_constraints (snd evd.evars) (snd d.evars))} + let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs} let evar_source evk d = try List.assoc evk d.history @@ -627,6 +628,8 @@ let define_sort_variable ({evars=(sigma,sm)}as d) u s = let pr_sort_constraints {evars=(_,sm)} = pr_sort_cstrs sm let solve_sort_constraints ({evars=(sigma,sm)} as d) = { d with evars = (sigma, solve_sort_cstrs sm) } +let clear_sort_constraints ({evars=(sigma,sm)} as d) = + { d with evars = (sigma, UniverseMap.empty) } (* This refreshes universes in types introducing sort variables; works only for inferred types (i.e. for @@ -639,7 +642,11 @@ let universes_to_variables_gen strict evd t = | Sort (Type u as us) when strict or u <> Univ.type0m_univ -> if not (is_sort_variable !evdref us) then let s', evd = new_sort_variable !evdref in - let evd = set_leq_sort_variable evd s' us in + let evd = + if not (Univ.is_univ_variable u) then + set_leq_sort_variable evd us s' + else evd + in evdref := evd; modified := true; mkSort s' else t | Prod (na,u,v) -> mkProd (na,u,refresh v) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 040cbf28c9..10ea2ca4dd 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -243,6 +243,7 @@ val set_leq_sort_variable : evar_defs -> sorts -> sorts -> evar_defs val set_eq_sort_variable : evar_defs -> sorts -> sorts -> evar_defs val define_sort_variable : evar_defs -> sorts -> sorts -> evar_defs val solve_sort_constraints : evar_defs -> evar_defs +val clear_sort_constraints : evar_defs -> evar_defs val universes_to_variables : evar_defs -> types -> evar_defs * types diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 0f8d2b860a..6c58e247a5 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -176,14 +176,13 @@ let oracle_order env cf1 cf2 = | Some k2 -> Some (Conv_oracle.oracle_order k1 k2) let is_trans_fconv_pb pb flags env sigma m n = - match pb with - | Cumul -> is_trans_fconv CUMUL flags env sigma m n - | ConvUnderApp _ -> is_trans_fconv CONV flags env sigma m n + let sigma' = clear_sort_constraints sigma in + is_trans_fconv (conv_pb_of pb) flags env sigma' m n let occur_meta_or_sortvar evd c = let rec occrec c = match kind_of_term c with | Meta _ -> raise Occur - | Sort s -> if Evd.is_sort_variable evd s then raise Occur + | Sort (Type u) -> raise Occur | _ -> iter_constr occrec c in try occrec c; false with Occur -> true @@ -369,7 +368,6 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag unirec_rec curenvnb pb b substn c1 (applist (c,(List.rev ks))) in - let m = whd_sort_variable sigma m and n = whd_sort_variable sigma n in if (if occur_meta_or_sortvar sigma m || occur_meta_or_sortvar sigma n then false else if (match flags.modulo_conv_on_closed_terms with | Some flags -> |