diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-03-03 21:45:42 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-03-03 22:15:10 +0100 |
| commit | 2d3916766d3f145643a994aa83174c98394d5baa (patch) | |
| tree | a1e687c049a1ad11484ed41507c06b55ddb959e6 /plugins/quote | |
| parent | 2f8a153dafb144b3fbf984680b4da7bc06c357c2 (diff) | |
Fix bug #3590, keeping evars that are not turned into named metas by
pattern_of_constr in an evar_map, as they can appear in the context
of said named metas, which is used by change. Not sure what to do in
the PEvar case, which never matches anyway according to Constr_matching.matches.
Diffstat (limited to 'plugins/quote')
| -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 637e0e28d..2a2ef30fb 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 (snd (pattern_of_constr (Global.env()) Evd.empty f), Array.map aux args) + PApp (pi3 (pattern_of_constr (Global.env()) Evd.empty f), Array.map aux args) | Cast (c,_,_) -> aux c - | _ -> snd (pattern_of_constr (Global.env())(*FIXME*) Evd.empty c) + | _ -> pi3 (pattern_of_constr (Global.env())(*FIXME*) Evd.empty c) in aux bodyi |