diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-07-16 19:21:35 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-07-16 19:21:35 +0200 |
| commit | e4aa8f13680a81ec7e2ebe1281b20d5791d13440 (patch) | |
| tree | e18d74166cfb4978ba3af86ae96be135b526efeb /pretyping/recordops.ml | |
| parent | ebb53e68cdc935a85c4da10852be4f7f3b492ee2 (diff) | |
Fix universe instantiation with canonical structures.
Patch by Matthieu Sozeau.
Fixes #3819: "Error: Unsatisfied constraints" due to canonical
structure inference
Diffstat (limited to 'pretyping/recordops.ml')
| -rw-r--r-- | pretyping/recordops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 6dc0d1f3c..7fde7b7ac 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -190,7 +190,7 @@ let cs_pattern_of_constr t = (* Intended to always succeed *) let compute_canonical_projections (con,ind) = let env = Global.env () in - let ctx = Environ.constant_context env con in + let ctx = Univ.instantiate_univ_context (Environ.constant_context env con) in let u = Univ.UContext.instance ctx in let v = (mkConstU (con,u)) in let ctx = Univ.ContextSet.of_context ctx in |