diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 20 |
1 files changed, 12 insertions, 8 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 297f0a1a8e..1fdbbb4128 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 @@ -1230,7 +1234,7 @@ let pb_equal = function | Reduction.CONV -> Reduction.CONV let report_anomaly _ = - let e = UserError ("", Pp.str "Conversion test raised an anomaly") in + let e = UserError (None, Pp.str "Conversion test raised an anomaly") in let e = CErrors.push e in iraise e |