diff options
| author | coqbot-app[bot] | 2020-11-20 08:51:20 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-20 08:51:20 +0000 |
| commit | 57c85b0d54e54ca33238399cab3285ef34d4edd2 (patch) | |
| tree | 3b67df9afab90f5ae1d2aeddd3773a544dcbca95 /pretyping/recordops.mli | |
| parent | f264aabf59866ae0d18509a7757e69c26e82f508 (diff) | |
| parent | 7265df1cda297603cb4eb74362df4463171c316a (diff) | |
Merge PR #13386: Fixes #9971: a useless situation where the type of a primitive projection was wrongly supposed to be already inferred
Reviewed-by: gares
Diffstat (limited to 'pretyping/recordops.mli')
| -rw-r--r-- | pretyping/recordops.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 3be60d5e62..5b8dc8184a 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -67,6 +67,7 @@ val find_primitive_projection : Constant.t -> Projection.Repr.t option (** A cs_pattern characterizes the form of a component of canonical structure *) type cs_pattern = Const_cs of GlobRef.t + | Proj_cs of Projection.Repr.t | Prod_cs | Sort_cs of Sorts.family | Default_cs @@ -88,7 +89,7 @@ val pr_cs_pattern : cs_pattern -> Pp.t type cs = GlobRef.t * inductive -val lookup_canonical_conversion : (GlobRef.t * cs_pattern) -> constr * obj_typ +val lookup_canonical_conversion : Environ.env -> (GlobRef.t * cs_pattern) -> constr * obj_typ val register_canonical_structure : warn:bool -> Environ.env -> Evd.evar_map -> cs -> unit val subst_canonical_structure : Mod_subst.substitution -> cs -> cs |