diff options
| author | Gaëtan Gilbert | 2018-06-11 13:57:28 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-14 15:46:16 +0100 |
| commit | 06b29ed748a9d9b99c2c08a3788906dbad5417d2 (patch) | |
| tree | 5623fad28f68f9450ab7122f595ec1727f8f52bf /vernac | |
| parent | 71b9ad8526155020c8451dd326a52e391a9a8585 (diff) | |
Repair relevance marks in-kernel.
Prevent errors when under annotating binders.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/assumptions.ml | 2 | ||||
| -rw-r--r-- | vernac/record.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index 3773bc9c88..445f10ecc1 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -239,7 +239,7 @@ and traverse_inductive (curr, data, ax2ty) mind obj = Array.fold_left (fun accu oib -> let pspecif = Univ.in_punivs (mib, oib) in let ind_type = Inductive.type_of_inductive global_env pspecif in - let indr = oib.mind_relevant in + let indr = oib.mind_relevance in let ind_name = Name oib.mind_typename in Context.Rel.add (Context.Rel.Declaration.LocalAssum (make_annot ind_name indr, ind_type)) accu) Context.Rel.empty mib.mind_packets diff --git a/vernac/record.ml b/vernac/record.ml index 46b4074eaa..23274040b0 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -288,7 +288,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f let r = mkIndU (indsp,u) in let rp = applist (r, Context.Rel.to_extended_list mkRel 0 paramdecls) in let paramargs = Context.Rel.to_extended_list mkRel 1 paramdecls in (*def in [[params;x:rp]]*) - let x = make_annot (Name binder_name) mip.mind_relevant in + let x = make_annot (Name binder_name) mip.mind_relevance in let fields = instantiate_possibly_recursive_type (fst indsp) u mib.mind_ntypes paramdecls fields in let lifted_fields = Termops.lift_rel_context 1 fields in let primitive = |