diff options
| author | Pierre-Marie Pédrot | 2015-07-27 14:28:15 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-07-27 14:28:15 +0200 |
| commit | aff5a1aaeb9b50c60ff32b7d5336a44fd18428ee (patch) | |
| tree | 39d21c9798b9ce7fb59892414f71fb60be61bcde /plugins | |
| parent | 05f22a5d6d5b8e3e80f1a37321708ce401834430 (diff) | |
| parent | cb145fa37d463210832c437f013231c9f028e1aa (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/extraction.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 080512b273..6ae519ef60 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -633,7 +633,8 @@ 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 (Projection.constant p) Univ.Instance.empty (c :: args) + let term = Retyping.expand_projection env (Evd.from_env env) p c [] in + extract_term env mle mlt term 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]. *) |