diff options
author | 2015-07-22 17:26:49 +0200 | |
---|---|---|
committer | 2015-07-22 17:26:49 +0200 | |
commit | 754775e39b5fa0342a1f4a46cbce0fc98d569d9d (patch) | |
tree | d907f1303514d557b901f949d5b02cc165a9992d /plugins/extraction/extraction.ml | |
parent | c07a9f1e558ab55de3011cbfc9749391ed60c768 (diff) |
Extraction: fix primitive projection extraction.
Use expand projection to come back to the projection-as-constant encoding, dealing with parameters correctly.
Diffstat (limited to 'plugins/extraction/extraction.ml')
-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 080512b27..6ae519ef6 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]. *) |