diff options
| author | Gaëtan Gilbert | 2020-01-09 11:30:48 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-01-09 11:30:48 +0100 |
| commit | cf5f6b5d4ecbd8c74b932b0d1e9b0de0922e5588 (patch) | |
| tree | 3b3c75f239a537fba57d5cfefc3a472a075c3ef8 /pretyping/recordops.ml | |
| parent | a9a06ffbd8aa4b5491227b6ef0e63831101b913f (diff) | |
Fix build after merge of #11164
Diffstat (limited to 'pretyping/recordops.ml')
| -rw-r--r-- | pretyping/recordops.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 4046419bd5..3b918b5396 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -138,7 +138,7 @@ let find_primitive_projection c = *) type obj_typ = { - o_ORIGIN : Constant.t; + o_ORIGIN : GlobRef.t; o_DEF : constr; o_CTX : Univ.AUContext.t; o_INJ : int option; (* position of trivial argument if any *) @@ -212,7 +212,8 @@ let compute_canonical_projections env ~warn (gref,ind) = mkConstU (con, u), Environ.constant_value_in env (con,u) | GlobRef.VarRef id -> mkVar id, Option.get (Environ.named_body id env) - | GlobRef.ConstructRef _ | GlobRef.IndRef _ -> assert false in + | GlobRef.ConstructRef _ | GlobRef.IndRef _ -> assert false + in let sign,t = Reductionops.splay_lam env (Evd.from_env env) (EConstr.of_constr c) in let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in let t = EConstr.Unsafe.to_constr t in @@ -231,7 +232,7 @@ let compute_canonical_projections env ~warn (gref,ind) = match cs_pattern_of_constr nenv t with | patt, o_INJ, o_TCOMPS -> ((GlobRef.ConstRef proji_sp, (patt, t)), - { o_ORIGIN = con ; o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS }) + { o_ORIGIN = gref ; o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS }) :: acc | exception Not_found -> if warn then warn_projection_no_head_constant (sign, env, t, gref, proji_sp); |