diff options
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 33 |
1 files changed, 19 insertions, 14 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index f4269a2c5d..f2f922fd51 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -561,17 +561,22 @@ let is_rigid_head sigma flags t = | Lambda (_, _, _) | LetIn (_, _, _, _) | App (_, _) | Case (_, _, _, _) | Proj (_, _) -> false (* Why aren't Prod, Sort rigid heads ? *) -let force_eqs c = - Universes.Constraints.fold - (fun ((l,d,r) as c) acc -> - let c' = if d == Universes.ULub then (l,Universes.UEq,r) else c in - Universes.Constraints.add c' acc) - c Universes.Constraints.empty - -let constr_cmp pb sigma flags t u = +let force_eqs c = + let open Universes in + Constraints.fold + (fun c acc -> + let c' = match c with + (* Should we be forcing weak constraints? *) + | ULub (l, r) | UWeak (l, r) -> UEq (Univ.Universe.make l,Univ.Universe.make r) + | ULe _ | UEq _ -> c + in + Constraints.add c' acc) + c Constraints.empty + +let constr_cmp pb env sigma flags t u = let cstrs = - if pb == Reduction.CONV then EConstr.eq_constr_universes sigma t u - else EConstr.leq_constr_universes sigma t u + if pb == Reduction.CONV then EConstr.eq_constr_universes env sigma t u + else EConstr.leq_constr_universes env sigma t u in match cstrs with | Some cstrs -> @@ -579,7 +584,7 @@ let constr_cmp pb sigma flags t u = with Univ.UniverseInconsistency _ -> sigma, false | Evd.UniversesDiffer -> if is_rigid_head sigma flags t then - try Evd.add_universe_constraints sigma (force_eqs cstrs), true + try Evd.add_universe_constraints sigma (force_eqs cstrs), true with Univ.UniverseInconsistency _ -> sigma, false else sigma, false end @@ -736,7 +741,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e | Evar (evk,_ as ev), Evar (evk',_) when not (Evar.Set.mem evk flags.frozen_evars) && Evar.equal evk evk' -> - let sigma',b = constr_cmp cv_pb sigma flags cM cN in + let sigma',b = constr_cmp cv_pb env sigma flags cM cN in if b then sigma',metasubst,evarsubst else @@ -918,7 +923,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e and unify_not_same_head curenvnb pb opt (sigma, metas, evars as substn : subst0) cM cN = try canonical_projections curenvnb pb opt cM cN substn with ex when precatchable_exception ex -> - let sigma', b = constr_cmp cv_pb sigma flags cM cN in + let sigma', b = constr_cmp cv_pb env sigma flags cM cN in if b then (sigma', metas, evars) else try reduce curenvnb pb opt substn cM cN @@ -1087,7 +1092,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e else let sigma, b = match flags.modulo_conv_on_closed_terms with | Some convflags -> infer_conv ~pb:cv_pb ~ts:convflags env sigma m n - | _ -> constr_cmp cv_pb sigma flags m n in + | _ -> constr_cmp cv_pb env sigma flags m n in if b then Some sigma else if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with | Some (cv_id, cv_k), (dl_id, dl_k) -> |