diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 16 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 18 | ||||
| -rw-r--r-- | pretyping/unification.ml | 13 |
3 files changed, 29 insertions, 18 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 3ef0bb1b35..d06009dce5 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -401,14 +401,16 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty else evar_eqappr_x ts env' evd CONV out2 out1 in let rigids env evd sk term sk' term' = - let b,univs = Universes.eq_constr_universes term term' in - if b then + let univs = Universes.eq_constr_universes term term' in + match univs with + | Some univs -> ise_and evd [(fun i -> let cstrs = Universes.to_constraints (Evd.universes i) univs in try Success (Evd.add_constraints i cstrs) with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p)); (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk sk')] - else UnifFailure (evd,NotSameHead) + | None -> + UnifFailure (evd,NotSameHead) in let flex_maybeflex on_left ev ((termF,skF as apprF),cstsF) ((termM, skM as apprM),cstsM) vM = let switch f a b = if on_left then f a b else f b a in @@ -650,14 +652,16 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty allow this identification (first-order unification of universes). Otherwise fallback to unfolding. *) - let b,univs = Universes.eq_constr_universes term1 term2 in - if b then + let univs = Universes.eq_constr_universes term1 term2 in + match univs with + | Some univs -> ise_and i [(fun i -> try Success (Evd.add_universe_constraints i univs) with UniversesDiffer -> UnifFailure (i,NotSameHead) | Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p)); (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] - else UnifFailure (i,NotSameHead) + | None -> + UnifFailure (i,NotSameHead) and f2 i = (try if not (snd ts) then raise Not_found diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 0ab941b346..a85e493eae 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -681,13 +681,17 @@ let magicaly_constant_of_fixbody env reference bd = function match constant_opt_value_in env (cst,u) with | None -> bd | Some t -> - let b, csts = Universes.eq_constr_universes t bd in - let subst = Universes.Constraints.fold (fun (l,d,r) acc -> - Univ.LMap.add (Option.get (Universe.level l)) (Option.get (Universe.level r)) acc) - csts Univ.LMap.empty - in - let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in - if b then mkConstU (cst,inst) else bd + let csts = Universes.eq_constr_universes t bd in + begin match csts with + | Some csts -> + let subst = Universes.Constraints.fold (fun (l,d,r) acc -> + Univ.LMap.add (Option.get (Universe.level l)) (Option.get (Universe.level r)) acc) + csts Univ.LMap.empty + in + let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in + mkConstU (cst,inst) + | None -> bd + end with | Not_found -> bd diff --git a/pretyping/unification.ml b/pretyping/unification.ml index e73c5ffaf3..e2b3af7e97 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -558,19 +558,22 @@ let force_eqs c = c Universes.Constraints.empty let constr_cmp pb sigma flags t u = - let b, cstrs = + let cstrs = if pb == Reduction.CONV then Universes.eq_constr_universes t u else Universes.leq_constr_universes t u in - if b then - try Evd.add_universe_constraints sigma cstrs, b + match cstrs with + | Some cstrs -> + begin try Evd.add_universe_constraints sigma cstrs, true with Univ.UniverseInconsistency _ -> sigma, false | Evd.UniversesDiffer -> if is_rigid_head flags t then - try Evd.add_universe_constraints sigma (force_eqs cstrs), b + try Evd.add_universe_constraints sigma (force_eqs cstrs), true with Univ.UniverseInconsistency _ -> sigma, false else sigma, false - else sigma, b + end + | None -> + sigma, false let do_reduce ts (env, nb) sigma c = Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state |