diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-11-19 17:48:32 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-11-19 17:52:26 +0100 |
| commit | 9d47cc0af706ed1cd4ab87c2d402a0457a9b6a5c (patch) | |
| tree | bf7c7746400e696d4fb3f2e7c677e955f8a52066 /plugins/quote/quote.ml | |
| parent | 6ababf42b3f03926c30cfbd209436ec83a21769e (diff) | |
Fix bug #4433, removing hack on evars appearing in a pattern from a
constr, and the associated signature, not needed anymore.
Update CHANGES, no evar_map is produced by pattern_of_constr anymore.
Diffstat (limited to 'plugins/quote/quote.ml')
| -rw-r--r-- | plugins/quote/quote.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 2a2ef30fb..b72ebbc92 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -211,9 +211,9 @@ let compute_rhs bodyi index_of_f = let i = destRel (Array.last args) in PMeta (Some (coerce_meta_in i)) | App (f,args) -> - PApp (pi3 (pattern_of_constr (Global.env()) Evd.empty f), Array.map aux args) + PApp (pattern_of_constr (Global.env()) Evd.empty f, Array.map aux args) | Cast (c,_,_) -> aux c - | _ -> pi3 (pattern_of_constr (Global.env())(*FIXME*) Evd.empty c) + | _ -> pattern_of_constr (Global.env())(*FIXME*) Evd.empty c in aux bodyi |