diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-11 15:39:01 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:27:33 +0100 |
| commit | 536026f3e20f761e8ef366ed732da7d3b626ac5e (patch) | |
| tree | 571e44e2277b6d045d6c11fafca58b5ea6e43afa /plugins/extraction/extraction.ml | |
| parent | ca993b9e7765ac58f70740818758457c9367b0da (diff) | |
Cleaning up opening of the EConstr module in pretyping folder.
Diffstat (limited to 'plugins/extraction/extraction.ml')
| -rw-r--r-- | plugins/extraction/extraction.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 0c4fa7055..6559aeb08 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -599,6 +599,7 @@ let rec extract_term env mle mlt c args = extract_cons_app env mle mlt cp args | Proj (p, c) -> let term = Retyping.expand_projection env (Evd.from_env env) p (EConstr.of_constr c) [] in + let term = EConstr.Unsafe.to_constr term in extract_term env mle mlt term args | Rel n -> (* As soon as the expected [mlt] for the head is known, *) |