diff options
Diffstat (limited to 'plugins/extraction/extraction.ml')
| -rw-r--r-- | plugins/extraction/extraction.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index bbbc9bce7..aa0232d19 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -617,7 +617,7 @@ let rec extract_term env mle mlt c args = | Construct (cp,u) -> extract_cons_app env mle mlt cp u args | Proj (p, c) -> - extract_cst_app env mle mlt p Univ.Instance.empty (c :: args) + extract_cst_app env mle mlt (Projection.constant p) Univ.Instance.empty (c :: args) | Rel n -> (* As soon as the expected [mlt] for the head is known, *) (* we unify it with an fresh copy of the stored type of [Rel n]. *) |