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 | |
| parent | a9a06ffbd8aa4b5491227b6ef0e63831101b913f (diff) | |
Fix build after merge of #11164
| -rw-r--r-- | pretyping/recordops.ml | 7 | ||||
| -rw-r--r-- | pretyping/recordops.mli | 2 | ||||
| -rw-r--r-- | vernac/prettyp.ml | 4 |
3 files changed, 6 insertions, 7 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); diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 7eac0ddf52..fd156adc2c 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -73,7 +73,7 @@ type cs_pattern = | Default_cs 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 *) diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 8ced35c3be..b999ce9f3f 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -1003,9 +1003,7 @@ let print_canonical_projections env sigma grefs = | Const_cs y -> GlobRef.equal y gr | _ -> false end || - match gr with - | GlobRef.ConstRef con -> Names.Constant.equal c.o_ORIGIN con - | _ -> false + GlobRef.equal c.o_ORIGIN gr in let projs = List.filter (fun p -> List.for_all (match_proj_gref p) grefs) |